- Mar 12, 2024
-
-
Andre Maroneze authored
-
- Jul 31, 2023
-
-
David Bühler authored
In all files, all occurrences of "[eva] done for function" have been replaced by "[eva] Done for function".
-
- Jul 17, 2023
-
-
David Bühler authored
-
- May 09, 2023
-
-
- 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.
-
- Mar 21, 2022
-
-
Virgile Prevosto authored
- always remove FC's internal attribute everywhere before deciding whether a cast is needed. - ACSL and C decisions to cast are similar - only unroll type for checking equality. If a cast is needed, keep typedef (if any) as target
-
- Feb 08, 2022
-
-
Andre Maroneze authored
-
- Jan 14, 2022
-
-
Andre Maroneze authored
-
- Jan 06, 2022
-
-
Patrick Baudin authored
-
- Sep 03, 2020
-
-
François Bobot authored
-
François Bobot authored
-
- Jul 15, 2020
-
-
- May 25, 2020
-
-
David Bühler authored
Only one builtin for the allocation functions.
-
- Mar 08, 2019
-
-
Andre Maroneze authored
-
- Feb 05, 2019
-
-
Loïc Correnson authored
-
Andre Maroneze authored
-
- Jan 14, 2019
-
-
Loïc Correnson authored
-
- Dec 12, 2018
-
-
Andre Maroneze authored
-
- Dec 04, 2018
-
-
Andre Maroneze authored
-
- Dec 03, 2018
-
-
Valentin Perrelle authored
- Fix Value/Value#5 - Fix Value/Value#14
-
- Nov 28, 2018
-
-
David Bühler authored
-
Andre Maroneze authored
Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
-
Andre Maroneze authored
-
- Nov 23, 2018
-
-
Virgile Prevosto authored
[Ptests] preserve LOG after STDOPT directive See merge request frama-c/frama-c!2073
-
- Nov 22, 2018
-
-
David Bühler authored
-
- Nov 16, 2018
-
-
Andre Maroneze authored
-
Loïc Correnson authored
-
- Oct 31, 2018
-
-
Virgile Prevosto authored
This is absolutely not a sneaky attempt to relaunch a build (now that OCI seems in better shape) pushing a nearly empty commit.
-