- May 05, 2023
-
-
David Bühler authored
-
David Bühler authored
Retroactively updates the Changelog for Eva and Ivette. See merge request frama-c/frama-c!4175
-
- 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
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
(Outside of the Variable module, which still differentiates variables and lvalues for now.) Infers intervals about lvalues and not only variables. Registers in deps variables and lvalues for which an interval is inferred.
-
-
-
-
-
-
-
-
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-