Commit 786526f4 authored by Sylvain Dailler's avatar Sylvain Dailler

Removes model_trace added at parsing

Removes debug flag: debug_auto_model.
Some changes in counterexamples triggered by:
- (non counterexamples) transformations which have a specific case for
   model_trace but not for the new detection: this is intended as
   simplifications that would be done are often simplifications we want
   for counterexamples,
- Some locations are missing in variables introduced by SP/WP which should
  explain the rest.

This also disables projections for record in intro_projection_counterexmp.

Correct subst_filter to be consistent with new counterexample modification
parent b6e01c68
...@@ -2,46 +2,52 @@ Strongest Postcondition ...@@ -2,46 +2,52 @@ Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 6: Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
x, [] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 10: Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 12: Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 16: Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "0" }, "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
{"type" : "Integer" ,
"val" : "1" }] } } "val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 25: Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" }, "list" : [{"type" : "Integer" , "val" : "-1" }, {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 27: Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" }, "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 8:
A, [] = {"proj_name" : "B_proj_1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
...@@ -2,46 +2,52 @@ Weakest Precondition ...@@ -2,46 +2,52 @@ Weakest Precondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 6: Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
x, [] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 10: Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 12: Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 16: Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "0" }, "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
{"type" : "Integer" ,
"val" : "1" }] } } "val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 25: Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" }, "list" : [{"type" : "Integer" , "val" : "-1" }, {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 27: Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" }, "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Apply" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 8:
A, [] = {"proj_name" : "B_proj_1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
...@@ -2,58 +2,58 @@ Strongest Postcondition ...@@ -2,58 +2,58 @@ Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat) bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 6: Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
x, [] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Unknown (sat) bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 10: Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat) bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 12: Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat) bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 16: Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" }, "list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" ,
{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 25: Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" }, "list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "165" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "163" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" }, "val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "161" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "159" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" }, "val" : {"apply" : "Nil" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 27: Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" }, "list" : [{"type" : "Integer" , "val" : "21" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "10" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "9" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" }, "val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "7" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "8" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" }, "val" : {"apply" : "Nil" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown bench/ce/algebraic_type.mlw M g: Timeout or Unknown
...@@ -2,58 +2,58 @@ Weakest Precondition ...@@ -2,58 +2,58 @@ Weakest Precondition
bench/ce/algebraic_type.mlw M G: Unknown (sat) bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 6: Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
x, [] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Unknown (sat) bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 10: Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat) bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 12: Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat) bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 16: Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" }, "list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" ,
{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 25: Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" }, "list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "165" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "165" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "163" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "163" }, "val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "161" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "161" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "159" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "159" }, "val" : {"apply" : "Nil" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw: Counter-example model:File algebraic_type.mlw:
Line 27: Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" }, "list" : [{"type" : "Integer" , "val" : "21" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "10" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "9" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" }, "val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "7" },
{"type" : "Apply" , "val" : {"apply" : "Cons" , {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" , "list" : [{"type" : "Integer" , "val" : "8" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" }, "val" : {"apply" : "Nil" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g: Timeout or Unknown bench/ce/algebraic_type.mlw M g: Timeout or Unknown
...@@ -2,11 +2,10 @@ Strongest Postcondition ...@@ -2,11 +2,10 @@ Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 35: Line 16:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } }, "val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } } "val" : "0" } }] } }
Line 36: Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -18,9 +17,8 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , ...@@ -18,9 +17,8 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
bench/ce/array_mono.mlw A VC f2: Valid bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 38: Line 25:
a, [[@introduced], [@model_trace:a], a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" , [@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
...@@ -29,7 +27,8 @@ a, [[@introduced], [@model_trace:a], ...@@ -29,7 +27,8 @@ a, [[@introduced], [@model_trace:a],
"value" : {"type" : "Integer" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 40: Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
......
...@@ -2,11 +2,10 @@ Weakest Precondition ...@@ -2,11 +2,10 @@ Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 35: Line 16:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } }, "val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } } "val" : "0" } }] } }
Line 36: Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -18,9 +17,8 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , ...@@ -18,9 +17,8 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
bench/ce/array_mono.mlw A VC f2: Valid bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 38: Line 25:
a, [[@introduced], [@model_trace:a], a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" , [@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
...@@ -28,15 +26,14 @@ a, [[@introduced], [@model_trace:a], ...@@ -28,15 +26,14 @@ a, [[@introduced], [@model_trace:a],
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" , {"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 40: a, [] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" , {"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 41: Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......
...@@ -2,11 +2,10 @@ Strongest Postcondition ...@@ -2,11 +2,10 @@ Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 35: Line 16:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } }, "val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } } "val" : "0" } }] } }
Line 36: Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -18,16 +17,16 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , ...@@ -18,16 +17,16 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
bench/ce/array_mono.mlw A VC f2: Valid bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 38: Line 25:
a, [[@introduced], [@model_trace:a], a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" , [@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } }, "val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" , {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 40: Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" , {"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
......
...@@ -2,11 +2,10 @@ Weakest Precondition ...@@ -2,11 +2,10 @@ Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 35: Line 16:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } }, "val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } } "val" : "0" } }] } }
Line 36: Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -18,22 +17,20 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , ...@@ -18,22 +17,20 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
bench/ce/array_mono.mlw A VC f2: Valid bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw: Counter-example model:File array_mono.mlw:
Line 38: Line 25:
a, [[@introduced], [@model_trace:a], a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" , [@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } }, "val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" , {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 40: a, [] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" , {"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } } "val" : "2" } }] } }
Line 41: Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" , "val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } }, "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......
...@@ -2,13 +2,13 @@ Strongest Postcondition ...@@ -2,13 +2,13 @@ Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw: Counter-example model:File array_records.mlw:
Line 23: Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" , "value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" , "value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } } "value" : {"type" : "Integer" ,
i, [[@introduced], "val" : "5" } }] } }
[@model_trace:i]] = {"type" : "Integer" , i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
Line 27: Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -23,13 +23,13 @@ i, [[@introduced], ...@@ -23,13 +23,13 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw: Counter-example model:File array_records.mlw:
Line 23: Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" , "value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" , "value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } } "value" : {"type" : "Integer" ,
i, [[@introduced], "val" : "5" } }] } }
[@model_trace:i]] = {"type" : "Integer" , i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
Line 27: Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -44,13 +44,13 @@ i, [[@introduced], ...@@ -44,13 +44,13 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw: Counter-example model:File array_records.mlw:
Line 23: Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" , "value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" , "value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } } "value" : {"type" : "Integer" ,
i, [[@introduced], "val" : "5" } }] } }
[@model_trace:i]] = {"type" : "Integer" , i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
Line 27: Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" , a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
...@@ -65,18 +65,25 @@ i, [[@introduced], ...@@ -65,18 +65,25 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw: Counter-example model:File array_records.mlw:
Line 23: Line 23:
a, [[@introduced], [@model_trace:a], a, [[@introduced],
[@at:'Old:loc:location], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" , [@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" , "value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,