Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

it looks like ppx_import and ppx_deriving could be useful

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

provides a skeleton for kf comparison

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

a priori, we start from a well-ordered AST, so that not all symbols are
concerned by a possible recursion, but this nevertheless might be the case
for aggregate and function definitions, as well as ACSL types and
functions/predicates.

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

modulo implementation of correspondance between expressions

Virgile Prevosto authored 3 years ago and David Bühler committed 2 years ago

Mostly a mock-up at this point

turns out that Change**DoChildren**Post does not visit the **head** node.

mimicks what we are allowing in mergecil.

- always remove FC's internal attribute everywhere before deciding whether
  a cast is needed.
- ACSL and C decisions to cast are similar
- only unroll type for checking equality. If a cast is needed, keep
  typedef (if any) as target

attributes that are completely internal to Frama-C and do not have any impact
on the semantics of the underlying value should not lead to a cast node.

an antediluvian comment hinted at some weird behavior of gcc and
MSVC at that time, but gcc is now fully ISO compliant in this respect
Waiting for complaints against the MSVC machdep to see whether special
case is warranted there.

Keep the APIs of Visitor and Cil.visit* in sync

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Skips the visit of C codes.

David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Only visits functions and variables definitions.

Logic preprocessing should not need extra args, since they were already
supplied to the preprocessor during the first pass. Passing them again might
lead to warnings about symbol redefinitions.