- Feb 23, 2021
-
-
Basile Desloges authored
The `e-acsl-gcc.sh` only looked for the Frama-C executable in the `$PATH`. This commit updates the search for Frama-C to be able to detect the binary if installed in a folder not added to the path, or if running the script from the development sources.
-
Julien Signoles authored
[eacsl] Fix Frama-C options in e-acsl-gcc.sh See merge request frama-c/frama-c!3065
-
Loïc Correnson authored
[wp] new cfg control See merge request frama-c/frama-c!3026
-
Loïc Correnson authored
-
- Feb 22, 2021
-
-
Valentin Perrelle authored
[Eva] Context from the evaluation engine to domains queries See merge request frama-c/frama-c!3080
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
-
Loïc Correnson authored
# Conflicts: # src/kernel_services/ast_queries/ast_info.mli # src/plugins/wp/Generator.ml # src/plugins/wp/cfgWP.ml
-
- Feb 19, 2021
-
-
Virgile Prevosto authored
[kernel] merging admit lemmas & axioms See merge request frama-c/frama-c!3058
-
David Bühler authored
Informs the domain that the current evaluation is a subdivision of the complete evaluation. Evaluation engine: [root] is set to false for subdivided evaluations.
-
David Bühler authored
The context currently contains the fields: - root: is the queried expression the root expression being evaluated, or is it a subexpression? - sudivision: the maximum number of subdivisions for the current evaluation. - subdivided: is the evaluation being subdivided? [root] is always set to false for subdivided evaluations.
-
David Bühler authored
The abstract domain queries [extract_expr] and [extract_lval] have a new boolean parameter [root], which is true for the root expression being evaluated, and false for all its sub-expression and lvalues.
-
- Feb 18, 2021
-
-
Basile Desloges authored
[eacsl] Merge contracts between RTL and stdlib Closes #999 See merge request frama-c/frama-c!3032
-
Basile Desloges authored
-
Basile Desloges authored
The contracts are updated to mention the behaviors in the contracts of `stdlib.h` and satisfy Eva.
-
Basile Desloges authored
[eacsl] Merge the specifications from the RTL functions with the corresponding functions from the user's project
-
Basile Desloges authored
-
David Bühler authored
add source audit options See merge request frama-c/frama-c!2947
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
-
-
-
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-