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

a local can be referenced in the type of another one, hence we can't
compare them in the same environment and update said environment
afterwards.

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

actually, we visit the spec of a function at its first occurrence,
so that it is possible that some global logic definitions
that are used in the constract haven't been visited yet.

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

Specifically if a global declaration `x` occurs between a
function declaration `f` and the definition of `f` which uses `x`

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

Dereference of placeholder was occurring at toplevel and not under a closure,
leading to an assert failure if you tried to use it

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

also working oracle for AST diff test

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

take into account that varinfos can stem from kernel functions (namely if
we take their address), and that they are supposed to be declared before
we see them, so that we don't have to compare their types and attributes
at each use, but just check the entries in the environment (either local
or global depending on vglob).

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.