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

in case ppx rewriting depend upon each other, ocamlfind applies them in
the order in which they are found on the command line, merlin in _reverse_
order. We can't thus use the exact same list in both cases.

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

[ivette] The Learn More menu item points to the Frama-C website.

See merge request frama-c/frama-c!3722

[wp] Disable a Cint simplifier

Closes #1133

See merge request frama-c/frama-c!3715

Maxime Jacquemin authored 2 years ago and David Bühler committed 2 years ago

As it is supposed to be a general framework, it must not contain direct
references to Frama-C. Now, the 'Learn More' link can be set through an
ipc communication, thus letting the application built over Dome decides.

[ivette] insert command into history

See merge request frama-c/frama-c!3726