Commit 8e1de5b1 authored by Sylvain Dailler's avatar Sylvain Dailler

ce: printer_mapping's list_projections is now a string -> ident map

The projection is now recorded with its ident which allow us to rewrite
the projections in counterexamples. We use the id_string which is only an
approximation of what can be seen in the task (but it is close enough).
parent 8ed7c5ec
......@@ -34,6 +34,10 @@ IDE
now generates counterexamples
* added support for GTK3
Counterexamples
* Field names now use ident names instead of smt generated ones:
int32qtint -> int32'int
Provers
* support for Z3 4.8.1 (released Oct 16, 2018)
* support for Z3 4.8.3 (released Nov 20, 2018)
......
This diff is collapsed.
This diff is collapsed.
......@@ -6,28 +6,28 @@ Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
......@@ -6,28 +6,28 @@ Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
......@@ -6,28 +6,28 @@ Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
......@@ -6,28 +6,28 @@ Line 5:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
Line 8:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } } }] } }
......@@ -2,45 +2,45 @@ Strongest Postcondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 18:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -48,27 +48,27 @@ bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 28:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -76,32 +76,32 @@ bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Counter-example model:File array.mlw:
Line 32:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 34:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -2,45 +2,45 @@ Weakest Precondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 18:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -48,27 +48,27 @@ bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 28:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -76,32 +76,32 @@ bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Counter-example model:File array.mlw:
Line 32:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
[@at:'Old:loc:location] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 34:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
a, [[@introduced]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
......@@ -2,11 +2,11 @@ Strongest Postcondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
......@@ -15,15 +15,15 @@ the check fails with all inputs
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 21:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -31,15 +31,15 @@ bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 27:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -47,15 +47,15 @@ bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 33:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -2,11 +2,11 @@ Weakest Precondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
......@@ -15,15 +15,15 @@ the check fails with all inputs
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 21:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -31,15 +31,15 @@ bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 27:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -47,15 +47,15 @@ bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
two, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
Line 33:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
three, [[@model_trace:three]] = {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
......@@ -5,21 +5,21 @@ Counter-example model:File ref.mlw:
Line 18:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
File jlamp_projections.mlw:
Line 29:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
Line 30:
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
......@@ -28,13 +28,13 @@ bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
......
......@@ -5,21 +5,21 @@ Counter-example model:File ref.mlw:
Line 18:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
File jlamp_projections.mlw:
Line 29:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
Line 30:
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } } }] } }
......@@ -28,13 +28,13 @@ bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
......
......@@ -5,21 +5,21 @@ Counter-example model:File ref.mlw:
Line 18:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
File jlamp_projections.mlw:
Line 29:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
Line 30:
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
......@@ -28,13 +28,13 @@ bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
......
......@@ -5,21 +5,21 @@ Counter-example model:File ref.mlw:
Line 18:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
File jlamp_projections.mlw:
Line 29:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
Line 30:
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"proj_name" : "to_int" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } } }] } }
......@@ -28,13 +28,13 @@ bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
Line 42:
b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
......
......@@ -2,20 +2,20 @@ Strongest Postcondition
bench/ce/range_type.mlw Range_int VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32'int" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "5" } }
bench/ce/range_type.mlw Range_float VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 20:
x, [[@introduced]] = {"proj_name" : "tqtreal" , "type" : "Proj" ,
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "10" } }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "tqtreal" ,
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "t'real" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "10" } }
......@@ -2,20 +2,20 @@ Weakest Precondition
bench/ce/range_type.mlw Range_int VC f: Timeout or Unknown
Counter-example model:File range_type.mlw:
Line 7:
x, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "5" } }
Line 9:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32qtint" ,
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "int32'int" ,