- Apr 01, 2019
-
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Andre Maroneze authored
better handling of gotos when inserting destructors Closes #545 and #499 See merge request frama-c/frama-c!2103
-
Andre Maroneze authored
-
Andre Maroneze authored
[Inout] Avoids folding implicit zero-initializers of large arrays. See merge request frama-c/frama-c!2105
-
- Mar 29, 2019
-
-
David Bühler authored
Fixes a performance issue.
-
David Bühler authored
Fixes a performance issue.
-
Valentin Perrelle authored
Floating-point widening hints See merge request frama-c/frama-c!1776
-
Andre Maroneze authored
-
Valentin Perrelle authored
-
Andre Maroneze authored
-
Patrick Baudin authored
Remove option -wp-assert-check-only See merge request frama-c/frama-c!2210
-
Andre Maroneze authored
[Eva] Base: rewrites is_valid_offset and valid_offset Closes #631 See merge request frama-c/frama-c!2206
-
Andre Maroneze authored
[Libc] remove unnecessary include See merge request frama-c/frama-c!2213
-
Andre Maroneze authored
The extraneous include prevents gzip from compiling.
-
- Mar 28, 2019
-
-
David Bühler authored
It is now invalid to read/write an empty struct in an Invalid base (such as the null base).
-
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.
-
Patrick Baudin authored
-
Patrick Baudin authored
-
- 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 25, 2019
-
-
Patrick Baudin authored
-
Andre Maroneze authored
[fcscript] Add a script to monitor and summarize multiple analyses See merge request frama-c/frama-c!2208
-
Valentin Perrelle authored
-
- Mar 19, 2019
-
-
Andre Maroneze authored
Avoid alpha-conversion clashes Closes #618 See merge request frama-c/frama-c!2201
-
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
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
[Cabs2cil] Fix collision of anon comp field names Closes #626 See merge request frama-c/frama-c!2207
-
Virgile Prevosto authored
-
- Mar 18, 2019
-
-
Virgile Robles authored
-
Valentin Perrelle authored
[Libc] fix some minor issues See merge request frama-c/frama-c!2134
-
Virgile Robles authored
-
Andre Maroneze authored
[parsing] Allow attributes in declarator lists Closes #616 See merge request frama-c/frama-c!2202
-
Patrick Baudin authored
[WP] better fitting detection for C cast - with an algo more lazy See merge request frama-c/frama-c!2204
-
Patrick Baudin authored
[WP] better fitting detection for C cast See merge request frama-c/frama-c!2199
-