Skip to content

Commit c93c37b

Browse files
voidcvoidc
committed
Update proofs
1 parent 413456d commit c93c37b

Some content is hidden

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

54 files changed

+1546
-1133
lines changed

‎creusot/tests/should_fail/cycle.stderr‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ warning: unused import: `creusot_contracts::*`
66
|
77
= note: `#[warn(unused_imports)]` on by default
88

9-
error[creusot]: encountered a cycle during translation: [{DefId(0:5 ~ cycle[c4ca]::f)}, {DefId(0:6 ~ cycle[c4ca]::g)}, {DefId(0:5 ~ cycle[c4ca]::f)}]
9+
error[creusot]: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[c4ca]::f))}, {Item(DefId(0:6 ~ cycle[c4ca]::g))}, {Item(DefId(0:5 ~ cycle[c4ca]::f))}]
1010
--> cycle.rs:4:1
1111
|
1212
4 | pub fn f() {

‎creusot/tests/should_succeed/all_zero.mlcfg‎

Lines changed: 0 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -104,35 +104,6 @@ module CreusotContracts_Resolve_Impl1_Resolve
104104
val resolve (self : borrowed t) : bool
105105
ensures { result = resolve self }
106106

107-
end
108-
module Core_Ptr_NonNull_NonNull_Type
109-
use prelude.Opaque
110-
type t_nonnull 't =
111-
| C_NonNull opaque_ptr
112-
113-
end
114-
module Core_Marker_PhantomData_Type
115-
type t_phantomdata 't =
116-
| C_PhantomData
117-
118-
end
119-
module Core_Ptr_Unique_Unique_Type
120-
use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type
121-
use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type
122-
type t_unique 't =
123-
| C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
124-
125-
end
126-
module Alloc_Boxed_Box_Type
127-
use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
128-
type t_box 't 'a =
129-
| C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a
130-
131-
end
132-
module Alloc_Alloc_Global_Type
133-
type t_global =
134-
| C_Global
135-
136107
end
137108
module AllZero_AllZero_Interface
138109
use prelude.Int
@@ -152,9 +123,7 @@ module AllZero_AllZero
152123
use prelude.Borrow
153124
use prelude.Int
154125
use prelude.UInt32
155-
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
156126
use AllZero_List_Type as AllZero_List_Type
157-
use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
158127
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve2 with
159128
type t = AllZero_List_Type.t_list
160129
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with

‎creusot/tests/should_succeed/all_zero/why3session.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
<path name=".."/><path name="all_zero.mlcfg"/>
88
<theory name="AllZero_AllZero" proved="true">
99
<goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
10-
<proof prover="1"><result status="valid" time="0.06" steps="738"/></proof>
10+
<proof prover="1"><result status="valid" time="0.06" steps="739"/></proof>
1111
</goal>
1212
</theory>
1313
</file>

‎creusot/tests/should_succeed/all_zero/why3shapes.gz‎

0 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/bdd.mlcfg‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -155,9 +155,9 @@ module Bdd_Hashmap_Impl1_Add_Interface
155155
type v
156156
use prelude.Borrow
157157
use map.Map
158+
use Core_Option_Option_Type as Core_Option_Option_Type
158159
clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
159160
type self = k
160-
use Core_Option_Option_Type as Core_Option_Option_Type
161161
use map.Map
162162
use Bdd_Hashmap_MyHashMap_Type as Bdd_Hashmap_MyHashMap_Type
163163
clone CreusotContracts_Model_Impl3_ShallowModel_Stub as ShallowModel1 with
@@ -3314,7 +3314,7 @@ module Bdd_Impl10_Not
33143314
function Interp0.interp = Interp0.interp,
33153315
val Max0.mAX' = Max0.mAX',
33163316
function Leastvar0.leastvar = Leastvar0.leastvar
3317-
clone Bdd_Impl10_Node_Interface as Node1 with
3317+
clone Bdd_Impl10_Node_Interface as Node0 with
33183318
predicate Invariant0.invariant' = Invariant0.invariant',
33193319
predicate IsValidBdd0.is_valid_bdd = IsValidBdd0.is_valid_bdd,
33203320
function Leastvar0.leastvar = Leastvar0.leastvar,
@@ -3445,7 +3445,7 @@ module Bdd_Impl10_Not
34453445
BB14 {
34463446
_32 <- borrow_mut ( * self);
34473447
self <- { self with current = ( ^ _32) };
3448-
r1 <- ([#"../bdd.rs" 522 16 522 44] Node1.node _32 v childt1 childf1);
3448+
r1 <- ([#"../bdd.rs" 522 16 522 44] Node0.node _32 v childt1 childf1);
34493449
_32 <- any borrowed (Bdd_Context_Type.t_context);
34503450
goto BB15
34513451
}
@@ -3640,7 +3640,7 @@ module Bdd_Impl10_And
36403640
function Interp0.interp = Interp0.interp,
36413641
val Max0.mAX' = Max0.mAX',
36423642
function Leastvar0.leastvar = Leastvar0.leastvar
3643-
clone Bdd_Impl10_Node_Interface as Node1 with
3643+
clone Bdd_Impl10_Node_Interface as Node0 with
36443644
predicate Invariant0.invariant' = Invariant0.invariant',
36453645
predicate IsValidBdd0.is_valid_bdd = IsValidBdd0.is_valid_bdd,
36463646
function Leastvar0.leastvar = Leastvar0.leastvar,
@@ -3887,7 +3887,7 @@ module Bdd_Impl10_And
38873887
BB31 {
38883888
_76 <- borrow_mut ( * self);
38893889
self <- { self with current = ( ^ _76) };
3890-
r1 <- ([#"../bdd.rs" 568 16 568 44] Node1.node _76 v childt childf);
3890+
r1 <- ([#"../bdd.rs" 568 16 568 44] Node0.node _76 v childt childf);
38913891
_76 <- any borrowed (Bdd_Context_Type.t_context);
38923892
goto BB32
38933893
}

‎creusot/tests/should_succeed/binary_search.mlcfg‎

Lines changed: 1 addition & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -118,35 +118,6 @@ module CreusotContracts_Resolve_Resolve_Resolve
118118
val resolve (self : self) : bool
119119
ensures { result = resolve self }
120120

121-
end
122-
module Core_Ptr_NonNull_NonNull_Type
123-
use prelude.Opaque
124-
type t_nonnull 't =
125-
| C_NonNull opaque_ptr
126-
127-
end
128-
module Core_Marker_PhantomData_Type
129-
type t_phantomdata 't =
130-
| C_PhantomData
131-
132-
end
133-
module Core_Ptr_Unique_Unique_Type
134-
use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type
135-
use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type
136-
type t_unique 't =
137-
| C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
138-
139-
end
140-
module Alloc_Boxed_Box_Type
141-
use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
142-
type t_box 't 'a =
143-
| C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a
144-
145-
end
146-
module Alloc_Alloc_Global_Type
147-
type t_global =
148-
| C_Global
149-
150121
end
151122
module BinarySearch_Impl0_Index_Interface
152123
type t
@@ -170,10 +141,8 @@ module BinarySearch_Impl0_Index
170141
use prelude.UIntSize
171142
use prelude.Int
172143
use prelude.Borrow
173-
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
174-
use BinarySearch_List_Type as BinarySearch_List_Type
175-
use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
176144
use Core_Option_Option_Type as Core_Option_Option_Type
145+
use BinarySearch_List_Type as BinarySearch_List_Type
177146
clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with
178147
type self = BinarySearch_List_Type.t_list t
179148
clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
@@ -271,9 +240,7 @@ module BinarySearch_Impl0_Len
271240
use prelude.Int
272241
use prelude.UIntSize
273242
use prelude.Borrow
274-
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
275243
use BinarySearch_List_Type as BinarySearch_List_Type
276-
use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
277244
clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with
278245
type self = BinarySearch_List_Type.t_list t
279246
clone BinarySearch_Impl0_LenLogic as LenLogic0 with

‎creusot/tests/should_succeed/binary_search/why3session.xml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,12 @@
1212
</theory>
1313
<theory name="BinarySearch_Impl0_Index" proved="true">
1414
<goal name="index&#39;vc" expl="VC for index" proved="true">
15-
<proof prover="1"><result status="valid" time="0.03" steps="122"/></proof>
15+
<proof prover="1"><result status="valid" time="0.03" steps="120"/></proof>
1616
</goal>
1717
</theory>
1818
<theory name="BinarySearch_Impl0_Len" proved="true">
1919
<goal name="len&#39;vc" expl="VC for len" proved="true">
20-
<proof prover="1"><result status="valid" time="0.02" steps="113"/></proof>
20+
<proof prover="1"><result status="valid" time="0.02" steps="114"/></proof>
2121
</goal>
2222
</theory>
2323
<theory name="BinarySearch_BinarySearch" proved="true">

‎creusot/tests/should_succeed/binary_search/why3shapes.gz‎

0 Bytes
Binary file not shown.

‎creusot/tests/should_succeed/bug/387.mlcfg‎

Lines changed: 1 addition & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -10,40 +10,9 @@ module Core_Option_Option_Type
1010
| C_Some a -> a
1111
end
1212
end
13-
module Core_Ptr_NonNull_NonNull_Type
14-
use prelude.Opaque
15-
type t_nonnull 't =
16-
| C_NonNull opaque_ptr
17-
18-
end
19-
module Core_Marker_PhantomData_Type
20-
type t_phantomdata 't =
21-
| C_PhantomData
22-
23-
end
24-
module Core_Ptr_Unique_Unique_Type
25-
use Core_Marker_PhantomData_Type as Core_Marker_PhantomData_Type
26-
use Core_Ptr_NonNull_NonNull_Type as Core_Ptr_NonNull_NonNull_Type
27-
type t_unique 't =
28-
| C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
29-
30-
end
31-
module Alloc_Boxed_Box_Type
32-
use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
33-
type t_box 't 'a =
34-
| C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a
35-
36-
end
37-
module Alloc_Alloc_Global_Type
38-
type t_global =
39-
| C_Global
40-
41-
end
4213
module C387_Node_Type
4314
use prelude.Int
4415
use prelude.UInt32
45-
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
46-
use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
4716
use Core_Option_Option_Type as Core_Option_Option_Type
4817
type t_node =
4918
| C_Node (t_tree) uint32 (t_tree)
@@ -328,16 +297,14 @@ module C387_Impl0_Height
328297
clone CreusotContracts_Logic_Ord_Impl2_LeLog as LeLog0
329298
clone CreusotContracts_Logic_Ord_Impl2_GeLog as GeLog0
330299
clone CreusotContracts_Std1_Num_Impl10_DeepModel as DeepModel0
331-
use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
332-
use C387_Node_Type as C387_Node_Type
333-
use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
334300
clone Core_Cmp_Ord_Max_Interface as Max0 with
335301
type self = uint64,
336302
function DeepModel0.deep_model = DeepModel0.deep_model,
337303
predicate GeLog0.ge_log = GeLog0.ge_log,
338304
predicate LeLog0.le_log = LeLog0.le_log,
339305
predicate LtLog0.lt_log = LtLog0.lt_log,
340306
type DeepModelTy0.deepModelTy = int
307+
use C387_Node_Type as C387_Node_Type
341308
use Core_Option_Option_Type as Core_Option_Option_Type
342309
use C387_Tree_Type as C387_Tree_Type
343310
let rec cfg height [#"../387.rs" 16 4 16 31] [@cfg:stackify] [@cfg:subregion_analysis] (self : C387_Tree_Type.t_tree) : uint64

‎creusot/tests/should_succeed/cell/02.mlcfg‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -227,14 +227,14 @@ module C02_Impl1_Inv
227227
use prelude.Borrow
228228
use prelude.Int
229229
use prelude.UIntSize
230-
clone C02_Fib_Stub as Fib1 with
230+
clone C02_Fib_Stub as Fib0 with
231231
axiom .
232232
use Core_Option_Option_Type as Core_Option_Option_Type
233233
use C02_Fib_Type as C02_Fib_Type
234234
predicate inv [#"../02.rs" 70 4 70 43] (self : C02_Fib_Type.t_fib) (v : Core_Option_Option_Type.t_option usize) =
235235
[#"../02.rs" 72 12 75 13] match (v) with
236236
| Core_Option_Option_Type.C_None -> true
237-
| Core_Option_Option_Type.C_Some i -> UIntSize.to_int i = Fib1.fib (UIntSize.to_int (C02_Fib_Type.fib_ix self))
237+
| Core_Option_Option_Type.C_Some i -> UIntSize.to_int i = Fib0.fib (UIntSize.to_int (C02_Fib_Type.fib_ix self))
238238
end
239239
val inv [#"../02.rs" 70 4 70 43] (self : C02_Fib_Type.t_fib) (v : Core_Option_Option_Type.t_option usize) : bool
240240
ensures { result = inv self v }
@@ -665,7 +665,7 @@ module C02_FibMemo
665665
clone C02_Fib as Fib0 with
666666
axiom .
667667
clone C02_Impl1_Inv as Inv0 with
668-
function Fib1.fib = Fib0.fib
668+
function Fib0.fib = Fib0.fib
669669
clone CreusotContracts_Std1_Slice_Impl5_HasValue as HasValue0 with
670670
type t = C02_Cell_Type.t_cell (Core_Option_Option_Type.t_option usize) (C02_Fib_Type.t_fib)
671671
clone CreusotContracts_Std1_Slice_Impl5_InBounds as InBounds0 with

0 commit comments

Comments
 (0)