Commit 3d58982b authored by Sylvain Dailler's avatar Sylvain Dailler

When printing models, add labels associated to a model element name id

This way, (labels|tags|attributes) can be retrieved on counterexamples
names.
parent 1038e22b
......@@ -30,11 +30,11 @@ fi
run () {
printf " $2 ($1)... "
f="$2_$1"
$dir/../bin/why3prove.opt -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
$dir/../bin/why3prove.opt --debug print_labels -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' > "$f.out"
$dir/../bin/why3prove.opt -P "$1,counterexamples" --timelimit 1 --debug fast_wp -a split_vc "$2.mlw" | \
$dir/../bin/why3prove.opt --debug print_labels -P "$1,counterexamples" --timelimit 1 --debug fast_wp -a split_vc "$2.mlw" | \
sed 's/ ([0-9]\+\.[0-9]\+s)//' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
......
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
x, ["model", "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 = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
x, ["model", "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 = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
x, ["model", "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 = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
x, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -25,62 +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 = {"type" : "Integer" , "val" : "1" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "1" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
old i, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -88,10 +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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
old i, ["model", "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 = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -25,62 +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 = {"type" : "Integer" , "val" : "1" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "1" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
old i, ["model", "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 = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "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 = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
i, ["model", "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 = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "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 = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -88,10 +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 = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "175" }
i, ["model", "model_trace:i"] = {"type" : "Integer" ,
"val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
old i, ["model", "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 = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
a.length, ["model", "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 = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] }
a = {"type" : "Array" ,
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" } }] }
{"others" : {"type" : "Integer" , "val" : "0" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, ["model", "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" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -47,15 +50,17 @@ old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -63,11 +68,11 @@ old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
......@@ -75,29 +80,32 @@ 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 = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 12:
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
old a.elts, ["model", "model_trace:a.elts@old"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
old a.elts, ["model",
"model_trace:a.elts@old"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
......@@ -108,16 +116,18 @@ Line 16:
the check fails with all inputs
File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" , "val" : "0" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
a.elts, ["model", "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 = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "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 = {"type" : "Integer" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
a.length, ["model", "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 = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
a.length, ["model", "model_trace:a.length"] = {"type" : "Integer" ,
"val" : "2" }
a.elts, ["model", "model_trace:a.elts"] = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "6" } }] }
a = {"type" : "Array" ,
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" } }] }
{"others" : {"type" : "Integer" , "val" : "6" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
a, ["model", "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" ,
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7211" }
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" } },
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 = {"type" : "Integer" ,
"val" : "7211" }
old 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" ,
old a.length, ["model", "model_trace:a.length@old"] = {"type" : "Integer" ,
"val" : "5874" }
old a.elts, ["model",
"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" ,
"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 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "7211" }
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" } },
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 = {"type" : "Integer" ,
"val" : "7211" }
old a.elts = {"type" : "Array" ,