- May 10, 2023
-
-
-
-
-
-
-
-
-
-
-
Allan Blanchard authored
Fix/wp/double assumes normalization See merge request frama-c/frama-c!4181
-
Allan Blanchard authored
[Eva] User manual: updates section about the octagon domain. See merge request frama-c/frama-c!4180
-
- May 09, 2023
-
-
Allan Blanchard authored
[ci] add pathcrawler See merge request frama-c/frama-c!4179
-
- May 05, 2023
-
-
Loïc Correnson authored
-
Loïc Correnson authored
-
David Bühler authored
-
David Bühler authored
Retroactively updates the Changelog for Eva and Ivette. See merge request frama-c/frama-c!4175
-
Allan Blanchard authored
-
- May 04, 2023
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
- MR !4164: fixes interpretation of Eva annotations. - MR !3993: allows comments in .ya automata files and specifications about floating-point variables. Also, Eva shows the name of enumeration tags instead of their integer values. - MR !4147: ivette shows the status of uninitialized and escaping variables. - MR !4151: better display of large integer sets. - MR !4134: the values table can show the status of ACSL predicates, the values of C lvalues in these predicates, and the values of function parameters. - MR !4098: fixes a soundness bug of the equality domain. - MR !4065: fixes performances issues on programs with too many callsites. - MR !4015: fixes the bitwise domain on big-endian architecture. - MR !4046: better partitioning splits on ACSL predicates.
-
David Bühler authored
[Eva] octagons: octagons about pointers See merge request frama-c/frama-c!4032
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
Uses faster but approximating functions for [join], [narrow] and [add]: in resulting maps (m, i), the inverse map [i] may contain variables that do not appear in [m]. Do not fail when this is the case.
-
David Bühler authored
Fixes performance issues: the initialization of large arrays or structures can lead to a very large number of relations or intervals. Also, do not infer intervals on volatile lvalues.
-
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
-
David Bühler authored
-
David Bühler authored
- Includes both direct and indirect dependencies of variables. - Avoids using Base.SetLattice.project. - Properly catches Not_found error when a variable is not in relation in the state. Also fixes [get_var_bases] function on missing variables. This function is called by [relate] according to the [Relations] map, which is an over-approximation of the relations really inferred in the state — it can contains variables that do not belong to the state, so [get_var_bases] should not crash in that case.
-
David Bühler authored
-
David Bühler authored
-