- May 20, 2021
-
-
David Bühler authored
-
David Bühler authored
Only one split (either static or dynamic) can be active on the same term. If a new split is encountered while a split is aleady active on the same term, the old split is removed.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
- Apr 02, 2021
-
-
David Bühler authored
When two loops follow each other, the automatic loop unrolling is performed on the transition edge between the two, where the current statement (from Cil.CurrentLoc) is still the first loop. Adds a test for this case.
-
- Feb 16, 2021
-
-
Virgile Prevosto authored
-
- Jan 21, 2021
-
-
Andre Maroneze authored
-
- Mar 11, 2020
-
-
Valentin Perrelle authored
This reverts commit e9c60779
-
Valentin Perrelle 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
Prerequisite for new options or annotations to configure more finely the subdivisions. In partition.ml, the subdivisions are disabled. Other files always use the default value of subdivisions.
-
- Oct 21, 2019
-
-
David Bühler authored
-
David Bühler authored
The new option -eva-auto-loop-unroll defines the maximum limit of automatic loop unrolling.
-
- Sep 16, 2019
-
-
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.
-
- Jul 26, 2019
-
-
François Bobot authored
Add migration script
-
- Apr 15, 2019
-
-
David Bühler authored
-
David Bühler authored
And not at each application of the split action.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
join_duplicate_keys replaces the code `of_partition (to_partition)` in trace_partitioning, and is probably more efficient. filter_map is applied to flows instead of partitions.
-
David Bühler authored
Creates stamps according to the evaluation of the returned expression in states.
-
David Bühler authored
-
David Bühler authored
Moves function split_by_evaluation from evaluation to partition. Moves function split_final_state from transfer_stmt to partition. New partitioning action Restrict, that restricts the rationing according to the evaluation of an expression into some expected values.
-
David Bühler authored
-
David Bühler authored
split_monitors are created and internally used by partition. New type split_kind to distinguish between static and dynamic splits, instead of using different constructors in the action type.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
-
-
David Bühler authored
-
-
-
-
-