Commit b174a9c0 authored by Sylvain Dailler's avatar Sylvain Dailler

ce bench: Update map for future use in the documentation

parent 4f4b4b4c
Pipeline #58314 passed with stages
in 84 minutes
theory ModelMap
use map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
module M
use int.Int
......@@ -42,3 +33,12 @@ module M
x := Map.set !x 0 true
end
theory ModelMap
use map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
Strongest Postcondition
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "43" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/map.mlw M VC test_map: Timeout or Unknown
Counter-example model:File map.mlw:
Line 16:
Line 7:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 17:
Line 8:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -25,7 +15,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 19:
Line 10:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -34,34 +24,21 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : "0" } }] } }] } }
bench/ce/map.mlw M VC test_map_multidim1: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
File map.mlw:
Line 22:
Counter-example model:File map.mlw:
Line 13:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 23:
Line 14:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 25:
Line 16:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
......@@ -78,19 +55,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"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 27:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -98,7 +64,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 28:
Line 19:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -110,7 +76,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 32:
Line 23:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -138,13 +104,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
File map.mlw:
Line 34:
Line 25:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 35:
Line 26:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -152,7 +118,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 37:
Line 28:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -176,13 +142,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
File map.mlw:
Line 39:
Line 30:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 40:
Line 31:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -190,7 +156,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 42:
Line 33:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Boolean" , "val" : true } },
......@@ -198,3 +164,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 41:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "43" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Weakest Precondition
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "43" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/map.mlw M VC test_map: Timeout or Unknown
Counter-example model:File map.mlw:
Line 16:
Line 7:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 17:
Line 8:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -25,7 +15,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 19:
Line 10:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -34,34 +24,21 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : "0" } }] } }] } }
bench/ce/map.mlw M VC test_map_multidim1: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
File map.mlw:
Line 22:
Counter-example model:File map.mlw:
Line 13:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 23:
Line 14:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 25:
Line 16:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Array" ,
......@@ -78,19 +55,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"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 27:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -98,7 +64,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 28:
Line 19:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -110,7 +76,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "1" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }] } }
Line 32:
Line 23:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -138,13 +104,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
File map.mlw:
Line 34:
Line 25:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 35:
Line 26:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -152,7 +118,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 37:
Line 28:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -176,13 +142,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
File map.mlw:
Line 39:
Line 30:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 40:
Line 31:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -190,7 +156,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 42:
Line 33:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Boolean" , "val" : true } },
......@@ -198,3 +164,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 41:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "43" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Strongest Postcondition
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
bench/ce/map.mlw M VC test_map: Timeout or Unknown
Counter-example model:File map.mlw:
Line 16:
Line 7:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 17:
Line 8:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -25,7 +15,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 19:
Line 10:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -34,31 +24,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : "2" } }] } }] } }
bench/ce/map.mlw M VC test_map_multidim1: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "2" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "2" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
File map.mlw:
Line 22:
Counter-example model:File map.mlw:
Line 13:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -67,7 +34,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 23:
Line 14:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -81,7 +48,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 25:
Line 16:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -107,19 +74,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
File map.mlw:
Line 27:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -129,7 +85,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 28:
Line 19:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -141,7 +97,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 32:
Line 23:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -169,13 +125,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
File map.mlw:
Line 34:
Line 25:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 35:
Line 26:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -183,7 +139,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 37:
Line 28:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -207,13 +163,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
File map.mlw:
Line 39:
Line 30:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 40:
Line 31:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -221,7 +177,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 42:
Line 33:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Boolean" , "val" : true } },
......@@ -229,3 +185,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 41:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
Weakest Precondition
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
bench/ce/map.mlw M VC test_map: Timeout or Unknown
Counter-example model:File map.mlw:
Line 16:
Line 7:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 17:
Line 8:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -25,7 +15,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 19:
Line 10:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -34,31 +24,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : "2" } }] } }] } }
bench/ce/map.mlw M VC test_map_multidim1: Timeout or Unknown
Counter-example model:File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "2" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "2" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
File map.mlw:
Line 22:
Counter-example model:File map.mlw:
Line 13:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -67,7 +34,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 23:
Line 14:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -81,7 +48,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] } }] } }
Line 25:
Line 16:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -107,19 +74,8 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
File map.mlw:
Line 27:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -129,7 +85,7 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 28:
Line 19:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -141,7 +97,7 @@ x, [[@introduced], [@field:0:contents],
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] } }] } }
Line 32:
Line 23:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Array" ,
......@@ -169,13 +125,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
File map.mlw:
Line 34:
Line 25:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 35:
Line 26:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -183,7 +139,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 37:
Line 28:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
......@@ -207,13 +163,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
File map.mlw:
Line 39:
Line 30:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 40:
Line 31:
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......@@ -221,7 +177,7 @@ x, [[@introduced], [@field:0:contents],
{"indice" : "1" , "value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
Line 42:
Line 33:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Boolean" , "val" : true } },
......@@ -229,3 +185,13 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Boolean" ,
"val" : false } }] } }] } }
bench/ce/map.mlw ModelMap t1: Unknown (sat)
Counter-example model:File map.mlw:
Line 41:
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
t, [[@introduced]] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment