- Apr 09, 2019
-
-
Virgile Prevosto authored
Fixes [external BTS 2432](https://bts.frama-c.com/view.php?id=2432)
-
- Apr 08, 2019
-
-
Virgile Prevosto authored
-
Virgile Prevosto authored
Fixes external issue 2433
-
Virgile Prevosto authored
-
- Apr 05, 2019
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
As it is redundant with all the information displayed during the analysis.
-
David Bühler authored
-
- Apr 04, 2019
-
-
David Bühler authored
-
- Apr 03, 2019
-
-
David Bühler authored
-
David Bühler authored
This can notably reduce the possible number of iterations after a widening.
-
- Apr 02, 2019
-
-
-
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
And not each time the option is changed.
-
David Bühler authored
As this can reset all saved states. Modified options will be set to their proper values anyway.
-
David Bühler authored
-
David Bühler authored
Only keeps -eva-precision. -eva-precision changes the paramaters even if they have already been set. -eva-precision -1 resets the options to their default value.
-
David Bühler authored
-
-
-
David Bühler authored
Quick configuration of a fast (but imprecise) or precise (but slow) analysis.
-
- Apr 01, 2019
-
-
David Bühler authored
-
David Bühler authored
This module type simplifies the signature of functors using evaluation functions.
-
David Bühler authored
Do not call enter_scope and leave_scope when no variables enter or leave the scope.
-
- Mar 29, 2019
-
-
David Bühler authored
Fixes a performance issue.
-
David Bühler authored
Fixes a performance issue.
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
The extraneous include prevents gzip from compiling.
-
- Mar 28, 2019
-
-
David Bühler authored
- shares and moves the functions [reduce_offset_by_validity] of Locations and Precise_locs into base.ml. - replaces the boolean argument ~for_writing into the new type access, that represents Read, Write or No_access. Without any access, offsets must point into or just beyond the base validity. - fixes the support of accesses of size 0: they are now invalid: + in bases with Invalid validity; + one past a base validity unless the base ends with an empty struct.
-
David Bühler authored
If needed, this boolean could be computed by the callers of these functions via Base.is_valid_offset. In Base, do not export offset_is_in_validity, that was only used to compute this boolean.
-
- Mar 27, 2019
-
-
Thibault Martin authored
Since commit #8783731f and #28139960 this option is not needed anymore. I updated LUncov (which was the only plugin using it) to remove it as well
-
- Mar 26, 2019
-
-
Valentin Perrelle authored
-
- Mar 25, 2019
-
-
Patrick Baudin authored
-
- Mar 19, 2019
-
-
Virgile Prevosto authored
-
Virgile Prevosto authored
Do not use two distinct undo stacks for taking care of which symbols are in use at a given program point. Let `Alpha` manages everything internally.
-
Virgile Prevosto authored
-