Commit ebeb4bda authored by Sylvain Dailler's avatar Sylvain Dailler

ce: first step for treatment of record with one field

Some cleaning of the counterexample testsuite remains to be done. Also,
some pretty-printing of the counterexamples in the ide.
parent 9e2d3d9a
......@@ -5,7 +5,7 @@ Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
......
......@@ -5,7 +5,7 @@ Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
......
......@@ -5,7 +5,7 @@ Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
......
......@@ -5,7 +5,7 @@ Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
......
......@@ -3,14 +3,16 @@ bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 16:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 35:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -23,7 +25,8 @@ bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 25:
a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -31,14 +34,15 @@ a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [] = {"type" : "Record" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@at:'Old], [@at:'Old:loc:location],
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -55,10 +59,10 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -3,14 +3,16 @@ bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 16:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 35:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -23,7 +25,8 @@ bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 25:
a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -31,14 +34,15 @@ a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [] = {"type" : "Record" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@at:'Old], [@at:'Old:loc:location],
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -55,10 +59,10 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -3,14 +3,16 @@ bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 16:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 35:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -23,19 +25,21 @@ bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 25:
a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [] = {"type" : "Record" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@at:'Old], [@at:'Old:loc:location],
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
......@@ -49,9 +53,9 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -3,14 +3,16 @@ bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 16:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 35:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -23,19 +25,21 @@ bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
Line 25:
a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [] = {"type" : "Record" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@at:'Old], [@at:'Old:loc:location],
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
......@@ -49,9 +53,9 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -65,7 +65,8 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -83,7 +84,8 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -101,7 +103,8 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -119,7 +122,8 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......
......@@ -65,7 +65,8 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -83,7 +84,8 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -101,7 +103,8 @@ i, [[@introduced],
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......@@ -119,7 +122,8 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
......
......@@ -2,110 +2,160 @@ Strongest Postcondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 12:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 18:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
......@@ -2,90 +2,109 @@ Weakest Precondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 12:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 18:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
Line 25:
x, [] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
Line 27:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18" } }] } }
......@@ -2,107 +2,156 @@ Strongest Postcondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }