- Apr 06, 2021
-
-
-
-
-
Virgile Prevosto authored
make nix attributes in default.nix extensible See merge request frama-c/frama-c!3104
-
David Bühler authored
[Eva] Fix a bug where added annotations were always slevel annotations See merge request frama-c/frama-c!3132
-
Valentin Perrelle authored
-
- Apr 02, 2021
-
-
Virgile Prevosto authored
-
Valentin Perrelle authored
[Eva] Improves the heuristic for automatic loop unrolling — episode 2 Closes Value/Value#135 See merge request frama-c/frama-c!2943
-
David Bühler authored
When two loops follow each other, the automatic loop unrolling is performed on the transition edge between the two, where the current statement (from Cil.CurrentLoc) is still the first loop. Adds a test for this case.
-
Virgile Prevosto authored
Simplifies the bug report gitlab template. See merge request frama-c/frama-c!3121
-
David Bühler authored
-
- Apr 01, 2021
-
-
Virgile Prevosto authored
-
- Mar 31, 2021
-
-
Andre Maroneze authored
[script] Fix exit code of `check_newline.sh` See merge request frama-c/frama-c!3127
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Basile Desloges authored
If the script find some errors, then the exit code is 1 instead of 0.
-
Michele Alberti authored
[Eva] The engines evaluates the location of ACSL \from clauses. See merge request frama-c/frama-c!3109
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
If an lvalue [lv1] from a loop exit condition is always assigned to the value of another lvalue [lv2] in the loop body, then the heuristic uses [lv2] as loop variant instead of [lv1]. This commit ensures that this replacement is only done if [lv1] is assigned to the value [lv2] in all possible path of the loop body.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
- The automatic loop unrolling now supports non-natural loops. - Improves the precision of the computation of delta increment.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
Domains can then use these locations. By lack of a cooperative evaluation engine of ACSL terms, only the cvalue domain is used to evaluate terms of \from clauses into locations.
-
François Bobot authored
Resolve "Specs des fonctions flottantes (math.h)" Closes #426 See merge request frama-c/frama-c!2405
-
Virgile Prevosto authored
-
- Mar 30, 2021
-
-
Basile Desloges authored
[eacsl] Fix address of end segment in RTL layout See merge request frama-c/frama-c!2979
-
Basile Desloges authored
-
David Bühler authored
-
- Mar 29, 2021
-
-
Basile Desloges authored
-
Valentin Perrelle authored
[bin/analysis-scripts] improve shell scripts thanks to shellcheck See merge request frama-c/frama-c!3106
-
Patrick Baudin authored
[tests] fixes test directives in two tests about save/load Closes #1036 See merge request frama-c/frama-c!3120
-