ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'remove_space_in_ident' into 'master'

Browse Source 
Remove space in ident

Closes #377

See merge request why3/why3!219
This commit is contained in:
DAILLER Sylvain
2019-08-23 14:47:33 +02:00
parent 0f477dac24 08857a1e85
commit b27bf68d81
242 changed files with 17685 additions and 17672 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
CHANGES.md
View File

@@ -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

8
bench/ce/oracles/array_mono_CVC4,1.7_SP.oracle
View File

@@ -1,6 +1,6 @@
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:

8
bench/ce/oracles/array_mono_CVC4,1.7_WP.oracle
View File

@@ -1,6 +1,6 @@
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:

9
bench/ce/oracles/array_mono_Z3,4.8.4_SP.oracle
View File

@@ -1,6 +1,6 @@
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" } }] } }

8
bench/ce/oracles/array_mono_Z3,4.8.4_WP.oracle
View File

@@ -1,6 +1,6 @@
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:

28
bench/ce/oracles/array_records_CVC4,1.7_SP.oracle
View File

@@ -1,5 +1,5 @@
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:

28
bench/ce/oracles/array_records_CVC4,1.7_WP.oracle
View File

@@ -1,5 +1,5 @@
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:

28
bench/ce/oracles/array_records_Z3,4.8.4_SP.oracle
View File

@@ -1,5 +1,5 @@
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:

28
bench/ce/oracles/array_records_Z3,4.8.4_WP.oracle
View File

@@ -1,5 +1,5 @@
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:

10
bench/ce/oracles/arrays_CVC4,1.7_SP.oracle
View File

@@ -1,6 +1,6 @@
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
bench/ce/arrays.mlw B VC f2: 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

10
bench/ce/oracles/arrays_CVC4,1.7_WP.oracle
View File

@@ -1,6 +1,6 @@
Weakest Precondition
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
bench/ce/arrays.mlw B VC f2: 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

10
bench/ce/oracles/arrays_Z3,4.8.4_SP.oracle
View File

@@ -1,6 +1,6 @@
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
bench/ce/arrays.mlw B VC f2: 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

10
bench/ce/oracles/arrays_Z3,4.8.4_WP.oracle
View File

@@ -1,6 +1,6 @@
Weakest Precondition
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
bench/ce/arrays.mlw B VC f2: 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

4
bench/ce/oracles/bv32_CVC4,1.7_SP.oracle
View File

@@ -1,5 +1,5 @@
Strongest Postcondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
@@ -20,7 +20,7 @@ File bv32.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:

4
bench/ce/oracles/bv32_CVC4,1.7_WP.oracle
View File

@@ -1,5 +1,5 @@
Weakest Precondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
@@ -20,7 +20,7 @@ File bv32.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:

4
bench/ce/oracles/bv32_Z3,4.8.4_SP.oracle
View File

@@ -1,5 +1,5 @@
Strongest Postcondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
@@ -20,7 +20,7 @@ File bv32.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:

4
bench/ce/oracles/bv32_Z3,4.8.4_WP.oracle
View File

@@ -1,5 +1,5 @@
Weakest Precondition
bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
@@ -20,7 +20,7 @@ File bv32.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'VC: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:

2
bench/ce/oracles/double_projection_CVC4,1.7_SP.oracle
View File

@@ -1,5 +1,5 @@
Strongest Postcondition
bench/ce/double_projection.mlw Test VC f: Unknown (sat)
bench/ce/double_projection.mlw Test f'VC: Unknown (sat)
Counter-example model:
File double_projection.mlw:
Line 17:

2
bench/ce/oracles/double_projection_CVC4,1.7_WP.oracle
View File

@@ -1,5 +1,5 @@
Weakest Precondition
bench/ce/double_projection.mlw Test VC f: Unknown (sat)
bench/ce/double_projection.mlw Test f'VC: Unknown (sat)
Counter-example model:
File double_projection.mlw:
Line 17:

2
bench/ce/oracles/double_projection_Z3,4.8.4_SP.oracle
View File

@@ -1,5 +1,5 @@
Strongest Postcondition
bench/ce/double_projection.mlw Test VC f: Unknown (sat)
bench/ce/double_projection.mlw Test f'VC: Unknown (sat)
Counter-example model:
File double_projection.mlw:
Line 17:

Some files were not shown because too many files have changed in this diff Show More