- May 03, 2022
-
-
-
-
it looks like ppx_import and ppx_deriving could be useful
-
-
-
-
-
-
-
-
provides a skeleton for kf comparison
-
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.
-
-
modulo implementation of correspondance between expressions
-
Mostly a mock-up at this point
-
-