- Jun 10, 2022
-
-
Patrick Baudin authored
-
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
-
- Jun 08, 2022
-
-
Patrick Baudin authored
header spec in git attributes See merge request frama-c/frama-c!3762
-
François Bobot authored
-
François Bobot authored
-
- Jun 07, 2022
-
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
-
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Andre Maroneze authored
[analysis-scripts] add mention about tool unavailability See merge request frama-c/frama-c!3774
-
Allan Blanchard authored
-
Allan Blanchard authored
Update Frama-CI data See merge request frama-c/frama-c!3773
-
Allan Blanchard authored
-
Allan Blanchard authored
-
Allan Blanchard authored
-
Andre Maroneze authored
-
Allan Blanchard authored
-
Allan Blanchard authored
-
- Jun 06, 2022
-
-
Julien Signoles authored
-
Julien Signoles authored
Remove Journal Closes #847 See merge request frama-c/frama-c!3738
-
- Jun 03, 2022
-
-
Virgile Prevosto authored
[Variadic] avoid musl-related test differences See merge request frama-c/frama-c!3769
-
Valentin Perrelle authored
[Eva] Fixes the evaluation engine when a domain oracle returns Bottom. See merge request frama-c/frama-c!3766
-
David Bühler authored
When the evaluation of any subexpression leads to Bottom, the evaluation of the complete expression returns only Bottom with no valuation: thus the valuation cache is no longer updated. However, when the evaluation of another expression requested by a domain through the oracle leads to Bottom, the evaluation of the primary expression may continue without leading to Bottom (domains are allowed to request the evaluation of 1/0 at any time, after all). In this case, we should properly update the cached valuation by binding Bottom to the expression requested by the domain, in case it should be used again in the evaluation (for instance if the requested evaluation was a subexpression of the primary target of the evaluation). And especially, if subdivided evaluations are enabled, the reference to the cached valuation must _always_ be reset after the oracle (even when it returns Bottom), as the cache has been used for successive evaluations with various hypotheses, and the last one is probably not sound in the general case.
-