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 9d7b426b authored by Sylvain Dailler's avatar Sylvain Dailler

Remove label model which is redundant with model_trace label. #108

parent 07b60cd3
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, ["model", "model_trace:x"] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
x, ["model_trace:x"] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, ["model", "model_trace:x"] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
x, ["model_trace:x"] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, ["model", "model_trace:x"] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
x, ["model_trace:x"] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, ["model", "model_trace:x"] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
x, ["model_trace:x"] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -27,71 +27,71 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "1" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i, ["model", "model_trace:i@old"] = {"type" : "Integer" ,
old i, ["model_trace:i@old"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -99,11 +99,11 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i, ["model", "model_trace:i@old"] = {"type" : "Integer" ,
old i, ["model_trace:i@old"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -27,71 +27,71 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "1" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i, ["model", "model_trace:i@old"] = {"type" : "Integer" ,
old i, ["model_trace:i@old"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -99,11 +99,11 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
i, ["model_trace:i"] = {"type" : "Integer" ,
"val" : "2" }
Line 25:
old i, ["model", "model_trace:i@old"] = {"type" : "Integer" ,
old i, ["model_trace:i@old"] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] }
a, ["model",
"model_trace:a", "model_trace:a@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] }
a, ["model_trace:a",
"model_trace:a@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", "model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
......@@ -32,47 +33,45 @@ a, ["model", "model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 32:
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
......@@ -80,14 +79,14 @@ bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 12:
old a.elts, ["model", "model_trace:a.elts@old"] = {"type" : "Array" ,
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -95,18 +94,17 @@ old a.elts, ["model", "model_trace:a.elts@old"] = {"type" : "Array" ,
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -116,18 +114,18 @@ Line 16:
the check fails with all inputs
File arrays.mlw:
Line 31:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "6" } }] }
a, ["model",
"model_trace:a", "model_trace:a@call"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "6" } }] }
a, ["model_trace:a",
"model_trace:a@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", "model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
......@@ -32,33 +33,9 @@ a, ["model", "model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "5874" }
a.elts, ["model",
"model_trace:a.elts"] = {"type" : "Array" , "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", "model_trace:a.length@old"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "5874" }
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" ,
a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
......@@ -77,37 +54,10 @@ old a.elts, ["model",
"val" : "8256" } }, {"indice" : "37" , "value" : {"type" : "Integer" ,
"val" : "9919" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "5874" }
a.elts, ["model",
"model_trace:a.elts"] = {"type" : "Array" , "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 32:
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
Line 27:
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "5874" }
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" ,
old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
......@@ -127,14 +77,55 @@ old a.elts, ["model",
"val" : "9919" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "7211" }
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" : "4" } }] }
Line 32:
old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "7211" }
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" : "4" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
......@@ -142,14 +133,14 @@ bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }