- Jul 19, 2023
-
-
Allan Blanchard authored
-
- Jul 18, 2023
-
-
Pierre Nigron authored
-
Pierre Nigron authored
-
Allan Blanchard authored
-
Allan Blanchard authored
-
Allan Blanchard authored
-
- Jul 17, 2023
-
-
Valentin Perrelle authored
[Eva] Fixes a bug on goto statement skipping local variable declarations. See merge request frama-c/frama-c!4245
-
Allan Blanchard authored
Easier use of make_machdep.py in installed Frama-C See merge request frama-c/frama-c!4215
-
Allan Blanchard authored
"[headers] temporary fix" See merge request frama-c/frama-c!4246
-
David Bühler authored
-
Jan Rochel authored
[e-acsl] rename misleading variable See merge request frama-c/frama-c!4240
-
Loïc Correnson authored
-
Loïc Correnson authored
-
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
-
-
Julien Signoles authored
-
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.
-
-
-
-