Skip to content

Commit 88cb570

Browse files
arnaudgolfousearnaudgolfouse
committed
Update tests
1 parent 085d7e3 commit 88cb570

File tree

224 files changed

+39877
-32905
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

224 files changed

+39877
-32905
lines changed

‎tests/creusot-contracts/creusot-contracts.coma

Lines changed: 19054 additions & 14185 deletions
Large diffs are not rendered by default.

‎tests/creusot-contracts/creusot-contracts/why3session.xml

Lines changed: 508 additions & 284 deletions
Large diffs are not rendered by default.

‎tests/creusot-contracts/creusot-contracts/why3shapes.gz

1.63 KB
Binary file not shown.

‎tests/should_fail/bug/01_resolve_unsoundness.coma

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs" 10 0 10 46]
2-
let%span s01_resolve_unsoundness = "01_resolve_unsoundness.rs" 12 16 12 17
3-
let%span s01_resolve_unsoundness'0 = "01_resolve_unsoundness.rs" 13 16 13 37
4-
let%span s01_resolve_unsoundness'1 = "01_resolve_unsoundness.rs" 15 17 15 22
5-
let%span s01_resolve_unsoundness'2 = "01_resolve_unsoundness.rs" 16 13 16 14
6-
let%span s01_resolve_unsoundness'3 = "01_resolve_unsoundness.rs" 9 10 9 29
7-
let%span svec = "../../../creusot-contracts/src/std/vec.rs" 72 26 72 44
8-
let%span svec'0 = "../../../creusot-contracts/src/std/vec.rs" 85 26 85 56
9-
let%span svec'1 = "../../../creusot-contracts/src/std/vec.rs" 21 14 21 41
2+
let%span s01_resolve_unsoundness = "01_resolve_unsoundness.rs" 9 10 9 29
3+
let%span s01_resolve_unsoundness'0 = "01_resolve_unsoundness.rs" 12 16 12 17
4+
let%span s01_resolve_unsoundness'1 = "01_resolve_unsoundness.rs" 13 16 13 37
5+
let%span s01_resolve_unsoundness'2 = "01_resolve_unsoundness.rs" 15 17 15 22
6+
let%span s01_resolve_unsoundness'3 = "01_resolve_unsoundness.rs" 16 13 16 14
7+
let%span svec = "../../../creusot-contracts/src/std/vec.rs" 21 14 21 41
8+
let%span svec'0 = "../../../creusot-contracts/src/std/vec.rs" 72 26 72 44
9+
let%span svec'1 = "../../../creusot-contracts/src/std/vec.rs" 85 26 85 56
1010
let%span sord = "../../../creusot-contracts/src/logic/ord.rs" 129 39 129 89
1111
let%span sord'0 = "../../../creusot-contracts/src/logic/ord.rs" 134 39 134 86
1212
let%span sord'1 = "../../../creusot-contracts/src/logic/ord.rs" 139 39 139 86
@@ -20,7 +20,7 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
2020
let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
2121
let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
2222
let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
23-
let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
23+
let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
2424
let%span smodel = "../../../creusot-contracts/src/model.rs" 62 8 62 22
2525

2626
use creusot.prelude.Opaque
@@ -52,10 +52,10 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
5252

5353
function view (self: t_Vec) : Seq.seq bool
5454

55-
axiom view_spec: forall self: t_Vec. [%#svec'1] Seq.length (view self) <= UInt64.t'int v_MAX
55+
axiom view_spec: forall self: t_Vec. [%#svec] Seq.length (view self) <= UInt64.t'int v_MAX
5656

5757
let rec new (return' (x:t_Vec))= any
58-
[ return''0 (result:t_Vec)-> {[%#svec] Seq.length (view result) = 0} (! return' {result}) ]
58+
[ return''0 (result:t_Vec)-> {[%#svec'0] Seq.length (view result) = 0} (! return' {result}) ]
5959

6060

6161
type t_Ordering =
@@ -109,28 +109,28 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
109109
[%#smodel] view self.current
110110

111111
let rec push (self_:MutBorrow.t t_Vec) (v:bool) (return' (x:()))= any
112-
[ return''0 (result:())-> {[%#svec'0] view self_.final = Seq.snoc (view'0 self_) v} (! return' {result}) ]
112+
[ return''0 (result:())-> {[%#svec'1] view self_.final = Seq.snoc (view'0 self_) v} (! return' {result}) ]
113113

114114

115115
meta "compute_max_steps" 1000000
116116

117117
let rec make_vec_of_size[#"01_resolve_unsoundness.rs" 10 0 10 46] (n:UInt64.t) (return' (x:t_Vec))= (! bb0
118118
[ bb0 = s0 [ s0 = new (fun (_ret:t_Vec) -> [ &out <- _ret ] s1) | s1 = bb1 ]
119-
| bb1 = s0 [ s0 = [ &i <- [%#s01_resolve_unsoundness] (0: UInt64.t) ] s1 | s1 = bb2 ]
119+
| bb1 = s0 [ s0 = [ &i <- [%#s01_resolve_unsoundness'0] (0: UInt64.t) ] s1 | s1 = bb2 ]
120120
| bb2 = bb2'0
121-
[ bb2'0 = {[@expl:loop invariant] [%#s01_resolve_unsoundness'0] UInt64.le (0: UInt64.t) i /\ UInt64.le i n'0}
121+
[ bb2'0 = {[@expl:loop invariant] [%#s01_resolve_unsoundness'1] UInt64.le (0: UInt64.t) i /\ UInt64.le i n'0}
122122
(! s0) [ s0 = bb3 ]
123123
[ bb3 = s0
124124
[ s0 = [ &_10 <- UInt64.le i n'0 ] s1 | s1 = any [ br0 -> {_10 = false} (! bb6) | br1 -> {_10} (! bb4) ] ]
125125

126126
| bb4 = s0
127127
[ s0 = MutBorrow.borrow_mut <t_Vec> {out}
128128
(fun (_ret:MutBorrow.t t_Vec) -> [ &_14 <- _ret ] [ &out <- _ret.final ] s1)
129-
| s1 = push {_14} {[%#s01_resolve_unsoundness'1] false} (fun (_ret:()) -> [ &_13 <- _ret ] s2)
129+
| s1 = push {_14} {[%#s01_resolve_unsoundness'2] false} (fun (_ret:()) -> [ &_13 <- _ret ] s2)
130130
| s2 = bb5 ]
131131

132132
| bb5 = s0
133-
[ s0 = UInt64.add {i} {[%#s01_resolve_unsoundness'2] (1: UInt64.t)}
133+
[ s0 = UInt64.add {i} {[%#s01_resolve_unsoundness'3] (1: UInt64.t)}
134134
(fun (_ret:UInt64.t) -> [ &i <- _ret ] s1)
135135
| s1 = bb2'0 ]
136136
]
@@ -147,7 +147,7 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
147147
| & _13: () = Any.any_l ()
148148
| & _14: MutBorrow.t t_Vec = Any.any_l () ]
149149

150-
[ return''0 (result:t_Vec)-> {[@expl:make_vec_of_size ensures] [%#s01_resolve_unsoundness'3] Seq.length (view result)
150+
[ return''0 (result:t_Vec)-> {[@expl:make_vec_of_size ensures] [%#s01_resolve_unsoundness] Seq.length (view result)
151151
= UInt64.t'int n}
152152
(! return' {result}) ]
153153

‎tests/should_fail/bug/1204.coma

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,19 @@ module M_1204__evil [#"1204.rs" 8 0 8 22]
22
let%span s1204 = "1204.rs" 6 11 6 16
33
let%span s1204'0 = "1204.rs" 7 10 7 11
44
let%span s1204'1 = "1204.rs" 9 4 9 16
5+
let%span swell_founded = "../../../creusot-contracts/src/well_founded.rs" 39 8 39 33
56

67
use mach.int.Int
78

9+
predicate well_founded_relation (self: int) (other: int) =
10+
[%#swell_founded] self >= 0 /\ self > other
11+
812
constant x : int
913

1014
function evil [#"1204.rs" 8 0 8 22] (x'0: int) : int
1115

1216
goal vc_evil: ([%#s1204] false)
13-
-> ([@expl:evil requires] [%#s1204] false) /\ 0 <= ([%#s1204'0] x) /\ ([%#s1204'0] - x) < ([%#s1204'0] x)
17+
-> ([@expl:evil requires] [%#s1204] false) /\ well_founded_relation ([%#s1204'0] x) ([%#s1204'0] - x)
1418
end
1519
module M_1204__wrong [#"1204.rs" 14 0 14 10]
1620
let%span s1204 = "1204.rs" 13 10 13 15

‎tests/should_fail/bug/1204/why3session.xml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,14 @@
99
<file format="coma">
1010
<path name=".."/><path name="1204.coma"/>
1111
<theory name="M_1204__evil" proved="true">
12-
<goal name="vc_evil&#39;0" proved="true">
12+
<goal name="vc_evil" proved="true">
1313
<proof prover="3"><result status="valid" time="0.021834" steps="0"/></proof>
1414
</goal>
1515
</theory>
1616
<theory name="M_1204__wrong">
17-
<goal name="vc_wrong&#39;0">
17+
<goal name="vc_wrong">
1818
<transf name="split_vc" >
19-
<goal name="vc_wrong&#39;0.0" expl="evil requires">
19+
<goal name="vc_wrong.0" expl="evil requires">
2020
<proof prover="0"><result status="unknown" time="0.013960" steps="8"/></proof>
2121
<proof prover="1"><result status="unknown" time="0.014204" steps="34"/></proof>
2222
<proof prover="2"><result status="unknown" time="0.011006" steps="47"/></proof>

‎tests/should_fail/bug/1204/why3shapes.gz

7 Bytes
Binary file not shown.

‎tests/should_fail/bug/222.coma

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,9 @@ module M_222__uses_invariant [#"222.rs" 40 0 40 41]
2929
| C_None
3030
| C_Some t_T
3131

32+
type t_Once =
33+
{ t_Once__0: t_Option }
34+
3235
predicate inv (_0: t_T)
3336

3437
predicate inv'0 (_0: t_Option)
@@ -39,17 +42,31 @@ module M_222__uses_invariant [#"222.rs" 40 0 40 41]
3942
| C_Some a_0 -> inv a_0
4043
end
4144

42-
type t_Once =
43-
{ t_Once__0: t_Option }
45+
predicate inv'1 (_0: t_Once)
46+
47+
axiom inv_axiom'0 [@rewrite]: forall x: t_Once [inv'1 x]. inv'1 x
48+
= match x with
49+
| {t_Once__0 = a_0} -> inv'0 a_0
50+
end
51+
52+
predicate invariant' (self: MutBorrow.t t_Once) =
53+
[%#sinvariant] inv'1 self.current /\ inv'1 self.final
54+
55+
predicate inv'2 (_0: MutBorrow.t t_Once)
56+
57+
axiom inv_axiom'1 [@rewrite]: forall x: MutBorrow.t t_Once [inv'2 x]. inv'2 x = invariant' x
4458

45-
predicate invariant' (self: MutBorrow.t t_Option) =
59+
predicate invariant''0 [#"222.rs" 29 4 29 30] (self: t_Once) =
60+
[%#s222'2] true
61+
62+
predicate invariant''1 (self: MutBorrow.t t_Option) =
4663
[%#sinvariant] inv'0 self.current /\ inv'0 self.final
4764

48-
predicate inv'1 (_0: MutBorrow.t t_Option)
65+
predicate inv'3 (_0: MutBorrow.t t_Option)
4966

50-
axiom inv_axiom'0 [@rewrite]: forall x: MutBorrow.t t_Option [inv'1 x]. inv'1 x = invariant' x
67+
axiom inv_axiom'2 [@rewrite]: forall x: MutBorrow.t t_Option [inv'3 x]. inv'3 x = invariant''1 x
5168

52-
let rec take (self_:MutBorrow.t t_Option) (return' (x:t_Option))= {[@expl:take 'self_' type invariant] [%#soption] inv'1 self_}
69+
let rec take (self_:MutBorrow.t t_Option) (return' (x:t_Option))= {[@expl:take 'self_' type invariant] [%#soption] inv'3 self_}
5370
any
5471
[ return''0 (result:t_Option)-> {inv'0 result}
5572
{[%#soption'0] result = self_.current /\ self_.final = C_None}
@@ -67,33 +84,16 @@ module M_222__uses_invariant [#"222.rs" 40 0 40 41]
6784
predicate resolve'1 (_0: t_Option) =
6885
resolve'0 _0
6986

70-
predicate inv'2 (_0: t_Once)
71-
72-
axiom inv_axiom'1 [@rewrite]: forall x: t_Once [inv'2 x]. inv'2 x
73-
= match x with
74-
| {t_Once__0 = a_0} -> inv'0 a_0
75-
end
76-
77-
predicate invariant''0 (self: MutBorrow.t t_Once) =
78-
[%#sinvariant] inv'2 self.current /\ inv'2 self.final
79-
80-
predicate inv'3 (_0: MutBorrow.t t_Once)
81-
82-
axiom inv_axiom'2 [@rewrite]: forall x: MutBorrow.t t_Once [inv'3 x]. inv'3 x = invariant''0 x
83-
8487
predicate resolve'2 (self: MutBorrow.t t_Once) =
8588
[%#sresolve'0] self.final = self.current
8689

8790
predicate resolve'3 (_0: MutBorrow.t t_Once) =
8891
resolve'2 _0
8992

90-
predicate invariant''1 [#"222.rs" 29 4 29 30] (self: t_Once) =
91-
[%#s222'2] true
92-
9393
meta "compute_max_steps" 1000000
9494

95-
let rec uses_invariant[#"222.rs" 40 0 40 41] (x:MutBorrow.t t_Once) (return' (x'0:()))= {[@expl:uses_invariant 'x' type invariant] [%#s222] inv'3 x}
96-
{[@expl:uses_invariant requires] [%#s222'0] invariant''1 x.current}
95+
let rec uses_invariant[#"222.rs" 40 0 40 41] (x:MutBorrow.t t_Once) (return' (x'0:()))= {[@expl:uses_invariant 'x' type invariant] [%#s222] inv'2 x}
96+
{[@expl:uses_invariant requires] [%#s222'0] invariant''0 x.current}
9797
(! bb0
9898
[ bb0 = s0
9999
[ s0 = {inv'0 (x'0.current).t_Once__0}
@@ -108,12 +108,12 @@ module M_222__uses_invariant [#"222.rs" 40 0 40 41]
108108
| s3 = -{resolve'1 _4}- s4
109109
| s4 = bb1 ]
110110

111-
| bb1 = s0 [ s0 = {[@expl:type invariant] inv'3 x'0} s1 | s1 = -{resolve'3 x'0}- s2 | s2 = bb2 ]
111+
| bb1 = s0 [ s0 = {[@expl:type invariant] inv'2 x'0} s1 | s1 = -{resolve'3 x'0}- s2 | s2 = bb2 ]
112112
| bb2 = return''0 {_0} ]
113113
)
114114
[ & _0: () = Any.any_l ()
115115
| & x'0: MutBorrow.t t_Once = x
116116
| & _4: t_Option = Any.any_l ()
117117
| & _5: MutBorrow.t t_Option = Any.any_l () ]
118-
[ return''0 (result:())-> {[@expl:uses_invariant ensures] [%#s222'1] invariant''1 x.final} (! return' {result}) ]
118+
[ return''0 (result:())-> {[@expl:uses_invariant ensures] [%#s222'1] invariant''0 x.final} (! return' {result}) ]
119119
end

‎tests/should_fail/bug/222/why3session.xml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,16 +9,16 @@
99
<file format="coma">
1010
<path name=".."/><path name="222.coma"/>
1111
<theory name="M_222__A__is_true">
12-
<goal name="vc_is_true&#39;0">
12+
<goal name="vc_is_true">
1313
<proof prover="0"><result status="unknown" time="0.021949" steps="3"/></proof>
1414
<proof prover="1"><result status="unknown" time="0.018668" steps="51"/></proof>
1515
<proof prover="3"><result status="unknown" time="0.015903" steps="64"/></proof>
1616
<proof prover="6"><result status="unknown" time="0.016368" steps="59"/></proof>
1717
</goal>
1818
</theory>
1919
<theory name="M_222__uses_invariant" proved="true">
20-
<goal name="vc_uses_invariant&#39;0" proved="true">
21-
<proof prover="6" timelimit="1"><result status="valid" time="0.008047" steps="2669"/></proof>
20+
<goal name="vc_uses_invariant" proved="true">
21+
<proof prover="6" timelimit="1"><result status="valid" time="0.008047" steps="2672"/></proof>
2222
</goal>
2323
</theory>
2424
</file>

‎tests/should_fail/bug/222/why3shapes.gz

-7 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)