Commit 153ca148 authored by Sylvain Dailler's avatar Sylvain Dailler

Update results of ce-bench

parent b4a8f43c
......@@ -14,6 +14,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -23,7 +29,21 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
......@@ -40,6 +60,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -49,4 +75,18 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "-1" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }
......@@ -14,6 +14,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -23,7 +29,33 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "165" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "163" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "161" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "159" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
......@@ -40,6 +72,12 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
......@@ -49,4 +87,30 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
This diff is collapsed.
......@@ -4,17 +4,21 @@ 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 int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "42" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
......@@ -22,9 +26,11 @@ 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 int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
......@@ -4,17 +4,21 @@ 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 int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "42" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Strongest Postcondition
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
......@@ -22,9 +26,11 @@ 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 int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "22" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
"val" : "84" }
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -2,146 +2,179 @@ Weakest Precondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"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
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "2" } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"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:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "2" } }
Line 34:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Strongest Postcondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "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:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 30:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
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" : "2" } }
......@@ -2,99 +2,121 @@ Weakest Precondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
the check fails with all inputs
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 21:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 27:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
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:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 33:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Strongest Postcondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
the check fails with all inputs
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 21:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 27:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
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:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
"val" : "2" }
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 14:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 33:
three, [[@model_trace:three]] = {"type" : "Integer" ,
"val" : "3" }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -3,24 +3,56 @@ bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "127" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "127" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 35:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Strongest Postcondition
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "127" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
Line 24:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "127" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 35:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 36:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
......@@ -3,24 +3,56 @@ bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "0" }
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 24: