Commit 3c3b7463 authored by Benedikt Becker's avatar Benedikt Becker

Merge branch 'describe-ce-values' into 'master'

Distinguish values of counterexamples for invariant preservation

See merge request !367
parents f88a55b6 c6da5555
module M1
use int.Int
let ref a = 0
let ref b = 0
let f () =
a <- -1;
a <- 1;
b <- 2;
while b < 10 do
variant { 10 - b }
invariant { b - a < 5 }
b <- b + a;
done
end
module M2
use int.Int
let g (ref a: int) ensures { a = old a + 1 } =
label X in
if a <> 10 then a <- a + 1;
assert { a = a at X }
end
\ No newline at end of file
Strongest Postcondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 8:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Weakest Precondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Strongest Postcondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 8:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
Weakest Precondition
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Valid
bench/ce/loop_ce.mlw M1 f'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 9:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 10:
b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 11:
[previous iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
Line 13:
[current iteration] a, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents], [@model_trace:b]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
Line 14:
[current iteration] b, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "6" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 22:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 23:
a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:a]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
a at X, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:X], [@model_trace:a], [@at:X:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Valid
bench/ce/loop_ce.mlw M2 g'vc: Timeout or Unknown
Counter-example model:
File loop_ce.mlw:
Line 20:
old a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "10" } }] } }
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -174,8 +174,8 @@ File record_one_field.mlw:
y, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -185,11 +185,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -86,15 +86,15 @@ File ref_mono.mlw:
x23, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
Line 38:
x23, [[@introduced], [@field:0:contents], [@model_trace:x23]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
"value" : {"type" : "Integer" , "val" : "401" } }] } }
old x23, [[@introduced], [@at:'Old], [@field:0:contents],
[@model_trace:x23], [@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
old y, [[@introduced], [@at:'Old], [@field:0:contents], [@model_trace:y],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,