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