- Apr 11, 2022
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
These functions uses the analysis status to return `Top or `Bottom if needed.
-
David Bühler authored
From Mark_noresults to Function_calls.
-
David Bühler authored
Must be consistent with [define_analysis_target].
-
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
Function [define_analysis_target] decides whether a builtin, the specification or the definition is used for the analysis of a given C function, according to Eva parameters. This function is then used in compute_functions.ml. [define_analysis_target] also decides whether the resulting states of an analysis should be saved, according to [-eva-results] parameters. Finally, [define_analysis_target] registers analyzed function calls in tables, with the caller/callsite and the defined analysis status.
-
David Bühler authored
-
Valentin Perrelle authored
[Eva] Converts more use of Db.Value to the new Eva API See merge request frama-c/frama-c!3689
-
Allan Blanchard authored
-
- Apr 08, 2022
-
-
-
David Bühler authored
Uses it in other plugins, instead of Db.Value.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
Maxime Jacquemin authored
Fix/ivette/eva details See merge request frama-c/frama-c!3692
-
- Apr 07, 2022
-
-
Julien Signoles authored
[eacsl] Increase the size of TLS in memory shadow model when necessary Closes e-acsl#197 See merge request frama-c/frama-c!3687
-
Thibaut Benjamin authored
-
Thibaut Benjamin authored
-
Thibaut Benjamin authored
-
-
-
David Bühler authored
[ivette] check import filename clashes See merge request frama-c/frama-c!3686
-
- Apr 06, 2022
-
-
Andre Maroneze authored
-
-
-
-
-
-
-
-