- Dec 07, 2022
-
-
Andre Maroneze authored
-
- Oct 04, 2022
-
-
- Sep 29, 2022
-
-
- Sep 26, 2022
-
-
Andre Maroneze authored
-
- Sep 09, 2022
-
-
Andre Maroneze authored
-
- Aug 30, 2022
-
-
Virgile Prevosto authored
-
- 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.
-
- Apr 22, 2022
-
-
Andre Maroneze authored
-
- Apr 14, 2022
-
-
Andre Maroneze authored
-
- Apr 11, 2022
-
-
David Bühler authored
-
- 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
-
Virgile Prevosto authored
attributes that are completely internal to Frama-C and do not have any impact on the semantics of the underlying value should not lead to a cast node.
-
- Mar 11, 2022
-
-
- Mar 10, 2022
-
-
- Mar 02, 2022
-
-
Andre Maroneze authored
-
- Feb 18, 2022
-
-
Andre Maroneze authored
These tests have missing specs, so the large amount of warnings is expected.
-
Andre Maroneze authored
There are still many missing specifications, but at least parsing should succeed for strictly POSIX-compliant code.
-
Andre Maroneze authored
-
- Feb 15, 2022
-
-
Andre Maroneze authored
-
Andre Maroneze authored
Frama-C does not yet support _Alignof and _Alignas, but this header helps parsing code and emitting a proper error message.
-
- Feb 10, 2022
-
-
Patrick Baudin authored
-
- Feb 08, 2022
-
-
Andre Maroneze authored
-
Andre Maroneze authored
-
- Jan 26, 2022
-
-
Andre Maroneze authored
-
-
- Jan 25, 2022
-
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
-
- Jan 20, 2022
-
-
- Jan 14, 2022
-
-
Andre Maroneze authored
-
Andre Maroneze authored
-
- Jan 06, 2022
-
-
Patrick Baudin authored
-
- Dec 10, 2021
-
-
Andre Maroneze authored
-
- Nov 18, 2021
-
-
Andre Maroneze authored
Clang 13 emits warnings related to uninitialized variables: variable 'r' is used uninitialized whenever 'if' condition is false [-Wsometimes-uninitialized] This is due to the fact that the assert(0) macro, when using Frama-C's libc, is expanded to __FC_assert. Since it is not known by the compiler, it cannot consider it as "noreturn" when the condition is zero. Note that adding '__attribute__ ((__noreturn__))' will not work: Frama-C will assume it never returns, even when the condition is true. Initializing the 'r' variables with a default value will not change the actual behavior, and will avoid the warnings.
-
- Nov 02, 2021
-
-
- Oct 19, 2021
-
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
-