Commit 4303c7e3 authored by Sylvain Dailler's avatar Sylvain Dailler

Update session and bench-ce

parent 786526f4
......@@ -33,12 +33,12 @@ Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "165" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "164" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "163" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "161" },
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "159" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -33,12 +33,12 @@ Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "165" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "164" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "163" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "161" },
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "159" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -28,8 +28,7 @@ Line 40:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"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" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
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" }
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" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 34:
x, [] = {"type" : "Integer" ,
"val" : "0" }
......@@ -5,7 +5,7 @@ Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
......@@ -14,52 +14,59 @@ Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"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 if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 36:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
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" }
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" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "2" }
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
the check fails with all inputs
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "2" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 31:
the check fails with all inputs
......@@ -5,7 +5,7 @@ Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
......@@ -14,52 +14,59 @@ Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "2" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
File if_assign.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
x, [[@introduced]] = {"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 if_assign.mlw:
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "2" }
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 36:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
......@@ -6,7 +6,7 @@ Counter-example model:File ref.mlw:
Line 18:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "42" } }
File int32.mlw:
Line 6:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
......@@ -15,5 +15,5 @@ r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "84" } }
......@@ -9,13 +9,13 @@ r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"val" : "22" } }
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "22" } }
"value" : {"type" : "Integer" , "val" : "84" } }
r, [[@introduced],
[@model_trace:r]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "84" } }
Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "42" } }
......@@ -6,12 +6,12 @@ Counter-example model:File ref.mlw:
Line 18:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "42" } }
File int32.mlw:
Line 6:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "22" } }
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -6,7 +6,7 @@ Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "22" } }
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } }
......@@ -17,5 +17,5 @@ r, [[@introduced],
Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "42" } }
......@@ -8,7 +8,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
Line 18:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -25,7 +25,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -39,7 +39,7 @@ a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -53,7 +53,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -67,7 +67,7 @@ a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -81,7 +81,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -95,7 +95,7 @@ a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......
......@@ -8,7 +8,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
Line 18:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -25,7 +25,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -41,7 +41,7 @@ a, [[@introduced],
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -52,7 +52,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -68,7 +68,7 @@ a, [[@introduced],
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
......@@ -84,7 +84,7 @@ two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -97,5 +97,5 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
......@@ -28,7 +28,7 @@ three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -47,7 +47,7 @@ three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
......@@ -66,5 +66,5 @@ three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
......@@ -31,7 +31,7 @@ Counter-example model:File record_one_field.mlw:
Line 13:
y, [[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
Line 15:
y, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -45,14 +45,14 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
y at 'Old, [[@introduced], [@at:'Old], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
Line 13:
y, [[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 15:
y, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -60,7 +60,7 @@ Line 41:
x23, [[@introduced],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 42:
x23, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -68,11 +68,11 @@ x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
y at 'Old, [[@introduced], [@at:'Old], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -80,12 +80,12 @@ Line 39:
y, [[@introduced],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 42:
x at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
x, [[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -93,7 +93,7 @@ Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
bench/ce/record_one_field.mlw M VC test_loop: Valid
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
......@@ -104,36 +104,36 @@ x, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"val" : "3" } }
Line 15:
x, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
"value" : {"type" : "Integer" , "val" : "2" } }
Line 39:
y, [[@introduced],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
Line 42:
x at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
x, [[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
Line 13:
x, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "-2" } }
"value" : {"type" : "Integer" , "val" : "0" } }
Line 39:
y, [[@introduced],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
Line 42:
x at 'Old, [[@at:'Old], [@at:'Old:loc:location],
[@at:L:loc:location],
......@@ -142,7 +142,7 @@ x at 'Old, [[@at:'Old], [@at:'Old:loc:location],
"val" : "-2" } }
x, [[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
Line 50:
x at 'Old, [[@introduced], [@at:'Old], [@model_trace:x],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
......
......@@ -31,7 +31,7 @@ Counter-example model:File record_one_field.mlw:
Line 13:
y, [[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
Line 15:
y, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -49,14 +49,14 @@ y at 'Old, [[@introduced],
[@at:'Old], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
Line 13:
y, [[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 15:
y, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -64,7 +64,7 @@ Line 41:
x23, [[@introduced],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 42:
x23, [] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
......@@ -75,15 +75,15 @@ x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
y at 'Old, [[@introduced], [@at:'Old], [@model_trace:y],