Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit dfab5cb0 authored by Sylvain Dailler's avatar Sylvain Dailler

fix #160

This fixes a problem in the wp generation and eval match where it was
possible to create new variables with same labels (including model_trace)
which does not have the same type. This results in bad typing for
counterexamples.
In particular, when only one region of a type is mutable we can project
directly during wp (now we do the same but with the corresponding
model_trace).
parent 95d3ef2d
......@@ -18,15 +18,15 @@ a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
a, ["model_trace:a@call"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 12:
a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a.elts, ["model_trace:a.elts@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......
......@@ -18,15 +18,15 @@ a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
a, ["model_trace:a@call"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 12:
a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a.elts, ["model_trace:a.elts@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
......@@ -143,41 +143,47 @@ bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "7211" }
"val" : "5874" }
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
"val" : "5737" } }, {"others" : {"type" : "Integer" ,
"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
"val" : "8257" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5338" , "value" : {"type" : "Integer" ,
"val" : "-7249" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
"val" : "-1" } }, {"indice" : "5466" , "value" : {"type" : "Integer" ,
"val" : "5876" } }, {"indice" : "-298" , "value" : {"type" : "Integer" ,
"val" : "1424" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
"val" : "-5876" } }, {"indice" : "-1547" , "value" : {"type" : "Integer" ,
"val" : "-2419" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
"val" : "-5875" } }, {"indice" : "5875" , "value" : {"type" : "Integer" ,
"val" : "5877" } }, {"indice" : "-299" , "value" : {"type" : "Integer" ,
"val" : "9873" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "8888" } }, {"indice" : "5709" , "value" : {"type" : "Integer" ,
"val" : "8256" } }, {"indice" : "37" , "value" : {"type" : "Integer" ,
"val" : "9919" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
Line 27:
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "7211" }
"val" : "5874" }
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
"val" : "5737" } }, {"others" : {"type" : "Integer" ,
"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
"val" : "8257" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5338" , "value" : {"type" : "Integer" ,
"val" : "-7249" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
"val" : "-1" } }, {"indice" : "5466" , "value" : {"type" : "Integer" ,
"val" : "5876" } }, {"indice" : "-298" , "value" : {"type" : "Integer" ,
"val" : "1424" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
"val" : "-5876" } }, {"indice" : "-1547" , "value" : {"type" : "Integer" ,
"val" : "-2419" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
"val" : "-5875" } }, {"indice" : "5875" , "value" : {"type" : "Integer" ,
"val" : "5877" } }, {"indice" : "-299" , "value" : {"type" : "Integer" ,
"val" : "9873" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "8888" } }, {"indice" : "5709" , "value" : {"type" : "Integer" ,
"val" : "8256" } }, {"indice" : "37" , "value" : {"type" : "Integer" ,
"val" : "9919" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Valid
......
......@@ -4,16 +4,16 @@ Line 17:
a, ["model_trace:a"] = {"type" : "Integer" ,
"val" : "5" }
Line 18:
TEMP_NAME, ["node_id=121",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=121",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : true }
Line 21:
TEMP_NAME, ["node_id=5454",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=5454",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : false }
Line 25:
TEMP_NAME, ["node_id=121",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=121",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : true }
bench/ce/if_decision_branch.mlw Other WP_parameter f : Unknown (other)
......
......@@ -4,16 +4,16 @@ Line 17:
a, ["model_trace:a"] = {"type" : "Integer" ,
"val" : "0" }
Line 18:
TEMP_NAME, ["node_id=121",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=121",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : false }
Line 21:
TEMP_NAME, ["node_id=5454",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=5454",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : false }
Line 25:
TEMP_NAME, ["node_id=121",
"model_trace:TEMP_NAME@assign"] = {"type" : "Boolean" ,
TEMP_NAME.sel_path, ["node_id=121",
"model_trace:TEMP_NAME.sel_path@assign"] = {"type" : "Boolean" ,
"val" : false }
bench/ce/if_decision_branch.mlw Other WP_parameter f : Unknown (other)
......
......@@ -3,16 +3,16 @@ bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r, ["model_trace:r"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents"] = {"type" : "Integer" ,
"val" : "22" }
Line 8:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "84" }
Line 9:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "42" }
Line 10:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "84" }
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
......@@ -20,7 +20,7 @@ bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r, ["model_trace:r"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents"] = {"type" : "Integer" ,
"val" : "22" }
Line 8:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
......
......@@ -3,16 +3,16 @@ bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r, ["model_trace:r"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents"] = {"type" : "Integer" ,
"val" : "22" }
Line 8:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "84" }
Line 9:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "42" }
Line 10:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents@call"] = {"type" : "Integer" ,
"val" : "84" }
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
......@@ -20,7 +20,7 @@ bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r, ["model_trace:r"] = {"type" : "Integer" ,
r.contents, ["model_trace:r.contents"] = {"type" : "Integer" ,
"val" : "22" }
Line 8:
r, ["model_trace:r@call"] = {"type" : "Integer" ,
......
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "3" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "3" }
Line 12:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "3" }
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "10" }
Line 10:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "9" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "5" }
Line 10:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "5" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "5" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 22:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 23:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@loop"] = {"type" : "Integer" ,
"val" : "3" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@loop"] = {"type" : "Integer" ,
"val" : "10" }
Line 22:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "12" }
Line 25:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "13" }
Line 26:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "12" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@loop"] = {"type" : "Integer" ,
"val" : "9" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@loop"] = {"type" : "Integer" ,
"val" : "2" }
Line 23:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "11" }
Line 25:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "11" }
Line 26:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@loop"] = {"type" : "Integer" ,
"val" : "3" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@loop"] = {"type" : "Integer" ,
"val" : "2" }
Line 25:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "5" }
Line 26:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@loop"] = {"type" : "Integer" ,
"val" : "3" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@call"] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@loop"] = {"type" : "Integer" ,
"val" : "3" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
c.contents, ["model_trace:c.contents@loop"] = {"type" : "Integer" ,
"val" : "11" }
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "3" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
......@@ -174,10 +174,10 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "7" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "3" }
Line 10:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
......@@ -192,7 +192,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -200,10 +200,14 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "0" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "0" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
......@@ -219,7 +223,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -227,14 +231,18 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "0" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "0" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "0" }
Line 23:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
......@@ -246,7 +254,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -254,10 +262,14 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "3" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "10" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "0" }
Line 22:
......@@ -273,7 +285,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -281,10 +293,14 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "9" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "2" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "0" }
Line 23:
......@@ -300,7 +316,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -308,10 +324,14 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "3" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "2" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "0" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
......@@ -324,10 +344,10 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents"] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
a, ["model_trace:a@try"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "3" }
Line 20:
c, ["model_trace:c@call"] = {"type" : "Integer" ,
......@@ -335,10 +355,14 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
Line 21:
a, ["model_trace:a@loop"] = {"type" : "Integer" ,
"val" : "3" }
a.contents, ["model_trace:a.contents@try"] = {"type" : "Integer" ,
"val" : "3" }
a, ["model_trace:a@try"] = {"type" : "Integer" ,
"val" : "3" }
c, ["model_trace:c@loop"] = {"type" : "Integer" ,
"val" : "11" }
c.contents, ["model_trace:c.contents@try"] = {"type" : "Integer" ,
"val" : "11" }
c, ["model_trace:c@try"] = {"type" : "Integer" ,
"val" : "11" }
Line 25:
......
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "0" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "3" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "3" }
Line 12:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "3" }
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6:
a, ["model_trace:a@init"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@init"] = {"type" : "Integer" ,
"val" : "7" }
Line 8:
b, ["model_trace:b"] = {"type" : "Integer" ,
b.contents, ["model_trace:b.contents"] = {"type" : "Integer" ,
"val" : "3" }
Line 10:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "9" }
Line 11:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, ["model_trace:a@call"] = {"type" : "Integer" ,
a.contents, ["model_trace:a.contents@call"] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File jlamp0.mlw:
Line 6: