- Jul 17, 2023
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
All variables local to a block are now introduced in domain states as soon as the analysis enters the block. This ensures all variables in scope have always been introduced in domain states, even when a goto statement jumps to a block after the declaration of some local variables, skipping their initializations (these variables would have been introduced in the states, but not initialized). As a downside, variables explicitly initialized at declaration enter the scope too early, as they should be introduced on the fly when encountering their [Local_init] instruction.
-
- Jul 13, 2023
-
-
David Bühler authored
Better callstacks in Eva See merge request frama-c/frama-c!4207
-
- Jul 12, 2023
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
Replaces [set_call_stack] by [init_call_stack]. Removes [legacy_call_stack], which is never used. Comments all function in the interface.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
- The callstack type is not private anymore. Only the current callstack in Eva_utils should not be modified without using push/pop; everywhere else, functions can freely create callstacks if needed. Removes function [change_thread], as it is now useless. - [pop] only returns the new callstack: this simplifies all its current uses. - new function [last_caller] returning the function from the penultimate call. - new function [pretty_debug] to allow using Hptmap on callstacks.
-
David Bühler authored
-
David Bühler authored
In Eva_utils, the reference to the current callstack is None until the analysis of the main function starts.
-
David Bühler authored
[register_initial_state] now takes the kernel_function as argument. This avoids using [Callstacks.top_kf] in the store.
-
-
-
-
-
-
-
Julien Signoles authored
[e-acsl] typing, translation: add some debug messages See merge request frama-c/frama-c!4233
-
Julien Signoles authored
[e-acsl] define Analyses_datatype.Profile.pretty See merge request frama-c/frama-c!4235
-
Jan Rochel authored
-
Allan Blanchard authored
[Dev] update reference configuration See merge request frama-c/frama-c!4236
-
- Jul 11, 2023
-
-
Andre Maroneze authored
-
Jan Rochel authored
Hitherto this function was defined as Datatype.undefined leading to an exception in Translate_terms.to_exp with -e-acsl-verbose 4 because of the call to Profile.pretty that takes place.
-
- Jul 07, 2023
-
-
Jan Rochel authored
Fix/alias/issue1278 Closes #1278 See merge request frama-c/frama-c!4232
-
Tristan Le Gall authored
-
Tristan Le Gall authored
-
- Jul 05, 2023
-
-
Maxime Jacquemin authored
[Eva] Greatly simplifies Abstractions.mli interface. See merge request frama-c/frama-c!4224
-
- Jul 04, 2023
-
-
Maxime Jacquemin authored
-