Commit 11b0ea10 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'session_vc_name' into 'master'

Change name of goal from "'VC" to "'vc"

See merge request !248
parents 0cbdbab1 336a4782
......@@ -16,7 +16,7 @@ Language
to give the name `Foo` to the corresponding hypothesis after introduction
* identifiers used for specification (resp. definition) of a function `foo`
have been renamed from `foo_spec` (resp. `foo_def`) to `foo'spec` (resp. `foo'def`) :x:
* identifiers used for goals `VC foo` have been renamed to `foo'VC`
* identifiers used for goals `VC foo` have been renamed to `foo'vc`
* identifiers used for record constructor `mk foo` have been renamed to `foo'mk` :x:
* the `alias` clause can now be used in program functions to force the aliasing
of function parameters and/or named returns
......
Strongest Postcondition
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: 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 f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: 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 array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: 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 f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: 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 array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: 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 f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: 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 array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: 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 f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 var_overwrite'VC: 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 f1'VC: Timeout or Unknown
bench/ce/arrays.mlw A f2'VC: Valid
bench/ce/arrays.mlw A f2'VC: Timeout or Unknown
bench/ce/arrays.mlw B f1'VC: Timeout or Unknown
bench/ce/arrays.mlw B f2'VC: Timeout or Unknown
bench/ce/arrays.mlw A f1'vc: Timeout or Unknown
bench/ce/arrays.mlw A f2'vc: Valid
bench/ce/arrays.mlw A f2'vc: Timeout or Unknown
bench/ce/arrays.mlw B f1'vc: Timeout or Unknown
bench/ce/arrays.mlw B f2'vc: Timeout or Unknown
Weakest Precondition
bench/ce/arrays.mlw A f1'VC: Timeout or Unknown
bench/ce/arrays.mlw A f2'VC: Valid
bench/ce/arrays.mlw A f2'VC: Timeout or Unknown
bench/ce/arrays.mlw B f1'VC: Timeout or Unknown