- Jun 17, 2022
-
-
David Bühler authored
Eva relies on the inout plugin to ensure that a function call has not modified the values of its concrete arguments, meaning that at the end of the call, the values of formal parameters can be backward propagated to the corresponding concrete arguments. This is useful when the values of some parameters have been reduced by the call, for instance by some preconditions. To this end, Eva uses the Inout callback Record_Inout_Callbacks from Db, but this callback was only applied by Inout for functions whose body is analyzed. This commit modifies Inout to also record its result through this callback on functions interpreted by a builtin or a specification, thus allowing a precise backward propagation of the values of formal parameters to concrete arguments in all cases.
-
Patrick Baudin authored
lint some files See merge request frama-c/frama-c!3809
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Loïc Correnson authored
[Wp] remove unused manual sections See merge request frama-c/frama-c!3807
-
Patrick Baudin authored
lint some files See merge request frama-c/frama-c!3808
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
- Jun 16, 2022
-
-
Andre Maroneze authored
-
Patrick Baudin authored
lint some files See merge request frama-c/frama-c!3806
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Virgile Prevosto authored
[kernel] fix \result type for ghost functions See merge request frama-c/frama-c!3778
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
-
- Jun 15, 2022
-
-
Allan Blanchard authored
[ci] downgrade ocamlfind See merge request frama-c/frama-c!3798
-
Allan Blanchard authored
-
- Jun 14, 2022
-
-
Virgile Prevosto authored
[Kernel] avoid recursion and fix layout of debug pretty-printers See merge request frama-c/frama-c!3784
-
Patrick Baudin authored
[hdrck] avoid double slashes when concatenating paths See merge request frama-c/frama-c!3795
-
Andre Maroneze authored
-
Virgile Prevosto authored
[Kernel] add predefined macros to avoid compiler warnings See merge request frama-c/frama-c!3787
-
- Jun 13, 2022
-
-
David Bühler authored
[Eva] Changes the opening comment of the not so experimental Results interface. See merge request frama-c/frama-c!3793
-
David Bühler authored
-
François Bobot authored
Fix E-ACSL header date See merge request frama-c/frama-c!3789
-
- Jun 10, 2022
-
-
Patrick Baudin authored
Fixes syntax on some ML files See merge request frama-c/frama-c!3790
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Allan Blanchard authored
-
Andre Maroneze authored
glibc 2.35 (https://lists.gnu.org/archive/html/info-gnu/2022-02/msg00002.html) defines macros __STDC_IEC_60559_BFP__ and __STDC_IEC_60559_COMPLEX__, which must be ignored to avoid redefinition warnings during logic preprocessing.
-
Allan Blanchard authored
[doc] fix headache commands when generating examples See merge request frama-c/frama-c!3785
-
Patrick Baudin authored
[Aorai] Fixes concurrent testing See merge request frama-c/frama-c!3782
-
Allan Blanchard authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Andre Maroneze authored
-