Commit 6c796347 authored by Sylvain Dailler's avatar Sylvain Dailler

Update ce-bench

parent a0c50301
......@@ -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" : "164" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "156" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
"list" : [{"type" : "Integer" , "val" : "154" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "150" }, {"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" : "164" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "156" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
"list" : [{"type" : "Integer" , "val" : "154" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "150" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -26,9 +26,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" ,
"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" } }] } }
Line 40:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
a, [[@introduced], [@model_trace: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" } },
......
......@@ -24,11 +24,17 @@ a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [] = {"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" } }] } }
Line 40:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......@@ -63,7 +63,14 @@ i, [[@introduced],
"val" : "-1" }
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.mlw:
Line 23:
a, [] = {"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" ,
"val" : "5" } }] } }
File array_records.mlw:
Line 23:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -76,14 +83,7 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"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" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
......@@ -93,7 +93,14 @@ i, [[@introduced],
"val" : "-1" }
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.mlw:
Line 23:
a, [] = {"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" ,
"val" : "5" } }] } }
File array_records.mlw:
Line 23:
a, [[@introduced],
[@at:'Old:loc:location],
......@@ -106,14 +113,7 @@ a, [[@introduced],
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"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" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
......@@ -135,15 +135,15 @@ a, [[@introduced],
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"type" : "Record" ,
Line 27:
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" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
......
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" }
Line 12:
x, [[@introduced]] = {"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" }
Line 18:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
......@@ -26,7 +42,8 @@ a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
the check fails with all inputs
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
......@@ -42,6 +59,6 @@ File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 34:
x, [] = {"type" : "Integer" ,
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
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" }
Line 12:
x, [[@introduced]] = {"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" }
Line 18:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
......@@ -26,7 +42,8 @@ a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 34:
the check fails with all inputs
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
......
......@@ -10,6 +10,11 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "15" }
Line 22:
path_selector, [] = {"type" : "Boolean" ,
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
Line 26:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : true }
......@@ -10,6 +10,11 @@ Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" }
Line 22:
path_selector, [] = {"type" : "Boolean" ,
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
Line 26:
TEMP_NAME, [[@introduced], [@model],
[@model_trace:TEMP_NAME]] = {"type" : "Boolean" ,
"val" : false }
......@@ -2,18 +2,20 @@ Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
File int32.mlw:
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } }
r, [[@introduced],
[@model_trace:r]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
......@@ -2,18 +2,20 @@ Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
File int32.mlw:
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } }
r, [[@introduced],
[@model_trace:r]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
......@@ -7,10 +7,11 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 8:
b, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 12:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
"val" : "3" }
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
......@@ -22,16 +23,25 @@ Line 8:
b, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 10:
a, [] = {"type" : "Integer" ,
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "9" }
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 22:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/jlamp0.mlw M VC p2: Valid
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
......@@ -43,11 +53,21 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "3" }
Line 24:
c, [] = {"type" : "Integer" ,
"val" : "4" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -58,11 +78,21 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 22:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "3" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "13" }
Line 26:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "12" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -73,9 +103,20 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "9" }
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "11" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "11" }
Line 26:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -87,6 +128,11 @@ Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
a, [] = {"type" : "Integer" ,
a, [] = {"type" : "Integer" , "val" : "3" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "3" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
......@@ -7,10 +7,11 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 8:
b, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 12:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
b, [[@introduced], [@model_trace:b]] = {"type" : "Integer" ,
"val" : "3" }
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
......@@ -22,16 +23,25 @@ Line 8:
b, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
Line 10:
a, [] = {"type" : "Integer" ,
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "9" }
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 22:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/jlamp0.mlw M VC p2: Valid
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
......@@ -43,11 +53,21 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "3" }
Line 24:
c, [] = {"type" : "Integer" ,
"val" : "4" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -58,11 +78,21 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 22:
the check fails with all inputs
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "3" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "13" }
Line 26:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "12" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -73,9 +103,20 @@ File jlamp0.mlw:
Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 23:
a, [] = {"type" : "Integer" ,
"val" : "9" }
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "11" }
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "11" }
Line 26:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -87,6 +128,11 @@ Line 6:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
a, [] = {"type" : "Integer" ,
a, [] = {"type" : "Integer" , "val" : "3" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "3" }
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
......@@ -33,16 +33,15 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -61,20 +60,24 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Counter-example model:File array.mlw:
Line 32:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -89,14 +92,10 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -26,9 +26,6 @@ Line 21:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -45,9 +42,6 @@ Line 27:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
......@@ -64,7 +58,4 @@ Line 33:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -17,8 +17,14 @@ x, [[@introduced]] = {"type" : "Array" , "val" : [{"indice" : "1" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 17:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
x, [] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] }
x, [[@introduced],
[@model_trace:x]] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -28,6 +34,10 @@ Line 18:
x, [] = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 20:
x, [] = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
File map.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
......@@ -41,15 +51,28 @@ Line 18:
x, [] = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 20:
x, [] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
File map.mlw:
Line 28:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
......@@ -60,10 +83,17 @@ x, [] = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 20:
x, [] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
File map.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -74,10 +104,17 @@ x, [] = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 20:
x, [] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
File map.mlw:
Line 40:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
"val" : [{"indice" : "0" , "value" : {"type" : "Boolean" , "val" : true } },
{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
......@@ -12,59 +12,129 @@ t, [[@introduced]] = {"type" : "Array" ,
bench/ce/map.mlw M VC test_map: Timeout or Unknown
Counter-example model:File map.mlw:
Line 16: