Commit 08857a1e authored by DAILLER Sylvain's avatar DAILLER Sylvain

Naming of ident: remove space in favor of "'"

- change prefix "mk " into suffix "'mk"
- change prefix "VC " into suffix "'VC"
parent 0f477dac
......@@ -15,6 +15,10 @@ Language
`requires Hyp { a = 3 }` tries to give the name `Hyp` to the corresponding
hypothesis after introduction. This uses the attribute [@hyp_name:] which is
now reserved.
* Ident suffix introduced for specification (resp definition) of a function
are renamed from "_spec" (resp. "_def" to "'spec" (resp. "'def" :x:
* Ident prefix introduced for goals "VC " and record constructor "mk "
becomes suffix "'VC" and "'mk".
Tools
* counterexamples given by `why3prove` are no longer printed using JSON
......
Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -22,8 +22,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -22,8 +22,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Strongest Postcondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -13,8 +13,8 @@ File array_mono.mlw:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "length" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......@@ -55,4 +55,3 @@ File array_mono.mlw:
{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -13,8 +13,8 @@ File array_mono.mlw:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "length" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Weakest Precondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Weakest Precondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Strongest Postcondition
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
bench/ce/arrays.mlw B VC f1: Timeout or Unknown