- Oct 13, 2022
-
-
David Bühler authored
To be removed in the next open-source release.
-
- Jul 19, 2022
-
-
David Bühler authored
Exports these functions in Eva.mli.
-
David Bühler authored
Used by the from plugin when option -from-verify-assigns is enabled.
-
- Jul 12, 2022
-
-
- Apr 11, 2022
-
-
David Bühler authored
-
David Bühler authored
Must be consistent with [define_analysis_target].
-
David Bühler authored
-
- Mar 03, 2022
-
-
Andre Maroneze authored
-
- Feb 23, 2022
-
-
Patrick Baudin authored
-
- Feb 17, 2022
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
- Feb 16, 2022
-
-
David Bühler authored
-
- Feb 15, 2022
-
-
- Jan 13, 2022
-
-
Allan Blanchard authored
- Info (expr_node) - IndexPI (PlusPI synonym)
-
- Feb 16, 2021
-
-
Virgile Prevosto authored
-
- Jan 21, 2021
-
-
Andre Maroneze authored
-
- Sep 07, 2020
-
-
David Bühler authored
-
- Mar 06, 2020
-
-
- Feb 12, 2020
-
-
David Bühler authored
-
- Feb 10, 2020
-
-
David Bühler authored
For abstract domains, the valuation is now a record of three functions: [find], [fold] and [find_loc]. Adds a function in the evaluation engine to convert Valuation maps into these records.
-
- Jan 23, 2020
-
-
David Bühler authored
New function Builtins.is_builtin_overridden that indicates whether a function is replaced by a builtin. This function remains correct after loading the result of a previous analysis, and can thus be used by other plugins using Eva's results. Thus, Db.Value.use_spec_instead_of_definition now uses this function.
-
- Sep 16, 2019
-
-
David Bühler authored
-
David Bühler authored
In abstract.ml, the structure of compound abstract values, locations and states carries the first class module of their leaf components as data.
-
David Bühler authored
Keys for abstract values, locations and states are created in structure.ml. Shapes are created in the respective modules Value, Location and Domain in abstract.ml.
-
David Bühler authored
These module definitions were previously in abstract_value, abstract_location and abstract_domain. They are now grouped in this new file for the three abstractions. These module types should only be useful for the engine, and need not to be visible in the implementation of the various abstractions. New module type Leaf in abstract_value, abstract_location and abstract_domain with the key identifying the module. The internal structure is no longer needed in these abstractions, and is instead built by the engine from this key. Keys are no longer exported outside the modules. For abstract domains, the key is automatically created by the functor Domain_builder.Complete from the domain name. Many changes throughout the analyzer: - in the engine, Abstract_value.{Internal|External} becomes Abstract.Value.{Internal|External}. - in the abstractions, Abstract_value.Internal becomes Abstract_value.Leaf.
-
- Sep 06, 2019
-
-
- Aug 02, 2019
-
-
David Bühler authored
-
- Apr 03, 2019
-
-
David Bühler authored
-
- Mar 28, 2019
-
-
David Bühler authored
- shares and moves the functions [reduce_offset_by_validity] of Locations and Precise_locs into base.ml. - replaces the boolean argument ~for_writing into the new type access, that represents Read, Write or No_access. Without any access, offsets must point into or just beyond the base validity. - fixes the support of accesses of size 0: they are now invalid: + in bases with Invalid validity; + one past a base validity unless the base ends with an empty struct.
-
- Feb 05, 2019
-
-
Loïc Correnson authored
-
- Jan 21, 2019
-
-
Loïc Correnson authored
(blind make headers from specifications)
-
- Jan 14, 2019
-
-
Loïc Correnson authored
-
- Dec 12, 2018
-
-
Andre Maroneze authored
-
- Dec 04, 2018
-
-
Andre Maroneze authored
-
- Dec 03, 2018
-
-
Valentin Perrelle authored
- Fix Value/Value#5 - Fix Value/Value#14
-