- 13 Jun, 2017 1 commit
-
-
Andrei Paskevich authored
eval_match should not destruct user-written quantifiers. For this purpose it preserves all quantifiers inside annotations. For the same purpose it now also preserves all quantifiers appearing inside terms in let-bindings (in particular, inside lambdas).
-
- 22 May, 2017 1 commit
-
-
Andrei Paskevich authored
We will want to use stop_split higher in the VC formulas.
-
- 29 Apr, 2017 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 20 Apr, 2017 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 16 Feb, 2017 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 30 Jan, 2017 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 29 Jan, 2017 4 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 28 Jan, 2017 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 23 Jan, 2017 1 commit
-
-
Andrei Paskevich authored
-
- 19 Jan, 2017 1 commit
-
-
Andrei Paskevich authored
-
- 15 Mar, 2016 1 commit
-
-
Andrei Paskevich authored
-
- 01 Mar, 2016 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
We only destruct n-tuples, unit types, and singleton records without invariants. We only inline projection-like functions for these types.
-
- 24 Jan, 2016 1 commit
-
-
Andrei Paskevich authored
also, rename asym_label to asym_split and keep_on_simp_label to keep_on_simp.
-
- 06 Oct, 2015 2 commits
-
-
David Hauzar authored
Record fields labeled with label model_trace:@hide_field will be not shown in counterexample.
-
David Hauzar authored
Previously, "." was automatically appended to names stored in model_trace label when creating variables corresponding to record fields in eval_match and when projecting record fields in the transformation intro_projections_counterexmp. Now, this is not done and "." must be given in model_trace label of the projection or record field. The reason is that for SPARK, character different from "." (e.g., "'" needs to be sometimes appended.
-
- 08 Sep, 2015 1 commit
-
-
David Hauzar authored
-
- 07 Sep, 2015 2 commits
-
-
David Hauzar authored
-
David Hauzar authored
-
- 04 Sep, 2015 1 commit
-
-
David Hauzar authored
Do not append '.' to the name of the variable representing field access if the field name is empty string (that is, if the field name should be ignored in counterexample).
-
- 03 Sep, 2015 3 commits
-
-
David Hauzar authored
were added to original labels.
-
David Hauzar authored
When eval_match creates new terms from original terms, all labels of the original terms are copied to the new terms. The exception are labels of the form "model_trace:*". These labels are not copied if both original terms and new terms contain this label.
-
David Hauzar authored
In wp, eval_match is used to replace record fields with simple variables of the same type. Originally, all labels from the variable that field was accessed were copied to new variables representing fields of this variable. Therefore also "model_trace:var_name" label was copied and thus the field had name "var_name" in the counterexample. This commit solves this problem by appending names of the fields to "model_trace:*" label of new variables representing record fields.
-
- 20 Mar, 2015 1 commit
-
-
Andrei Paskevich authored
-
- 19 Mar, 2015 1 commit
-
-
MARCHE Claude authored
-
- 05 Mar, 2015 1 commit
-
-
Martin Clochard authored
-
- 11 Jul, 2014 1 commit
-
-
Martin Clochard authored
This is to prevent quantified records from being decomposed by eval_match. e.g, assert { forall x:t. ... } was previously transformed to assert { forall x1:t1, x2:t2, x3:t3. ... } if x was a record type with fields x1,x2,x3. This changed the instantiation pattern, which could be harmful.
-
- 14 Mar, 2014 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 18 Jan, 2014 1 commit
-
-
Andrei Paskevich authored
-
- 10 Nov, 2013 1 commit
-
-
Andrei Paskevich authored
-