Update tests

creusot-rs · May 18, 2024 · 551a6ed · 551a6ed
1 parent 5d0c53a
commit 551a6ed
Show file tree

Hide file tree

Showing 52 changed files with 739 additions and 739 deletions.
diff --git a/creusot/tests/should_fail/cycle.stderr b/creusot/tests/should_fail/cycle.stderr
@@ -6,7 +6,7 @@ warning: unused import: `creusot_contracts::*`
   |
   = note: `#[warn(unused_imports)]` on by default
 
-error: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[f39e]::f))}, {Item(DefId(0:6 ~ cycle[f39e]::g))}, {Item(DefId(0:5 ~ cycle[f39e]::f))}]
+error: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[b375]::f))}, {Item(DefId(0:6 ~ cycle[b375]::g))}, {Item(DefId(0:5 ~ cycle[b375]::f))}]
  --> cycle.rs:4:1
   |
 4 | pub fn f() {

diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
@@ -470,14 +470,14 @@ module C100doors_F
     goto BB21
   }
   BB12 {
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _12;
     [#"../100doors.rs" 20 4 20 41] _17 <- ([#"../100doors.rs" 20 4 20 41] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem)));
     goto BB13
   }
   BB13 {
     [#"../100doors.rs" 20 4 20 41] produced <- _17;
     _17 <- any Snapshot.snap_ty (Seq.seq usize);
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] pass <- __creusot_proc_iter_elem;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] pass <- __creusot_proc_iter_elem;
     [#"../100doors.rs" 22 30 22 34] door <- pass;
     goto BB14
   }

diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg
@@ -1149,7 +1149,7 @@ module Hillel_InsertUnique
     goto BB24
   }
   BB18 {
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28;
     assert { [@expl:type invariant] inv4 _28 };
     assume { resolve6 _28 };
     [#"../hillel.rs" 84 4 84 111] _33 <- ([#"../hillel.rs" 84 4 84 111] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem)));
@@ -1160,7 +1160,7 @@ module Hillel_InsertUnique
     _33 <- any Snapshot.snap_ty (Seq.seq t);
     assert { [@expl:type invariant] inv2 produced };
     assume { resolve4 produced };
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] e <- __creusot_proc_iter_elem;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] e <- __creusot_proc_iter_elem;
     assert { [@expl:type invariant] inv5 __creusot_proc_iter_elem };
     assume { resolve7 __creusot_proc_iter_elem };
     assert { [@expl:assertion] [#"../hillel.rs" 86 24 86 57] e
@@ -1717,14 +1717,14 @@ module Hillel_Unique
     goto BB21
   }
   BB16 {
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _23;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _23;
     [#"../hillel.rs" 104 4 104 48] _28 <- ([#"../hillel.rs" 104 4 104 48] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem)));
     goto BB17
   }
   BB17 {
     [#"../hillel.rs" 104 4 104 48] produced <- _28;
     _28 <- any Snapshot.snap_ty (Seq.seq usize);
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem;
     [#"../hillel.rs" 108 26 108 27] _32 <- i;
     [#"../hillel.rs" 108 22 108 28] _33 <- Slice.length str;
     [#"../hillel.rs" 108 22 108 28] _34 <- _32 < _33;
@@ -2366,7 +2366,7 @@ module Hillel_Fulcrum
     goto BB12
   }
   BB10 {
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19;
     [#"../hillel.rs" 159 4 159 60] _24 <- ([#"../hillel.rs" 159 4 159 60] Snapshot.new (Seq.(++) (Snapshot.inner produced) (Seq.singleton __creusot_proc_iter_elem)));
     goto BB11
   }
@@ -2438,14 +2438,14 @@ module Hillel_Fulcrum
     return _0
   }
   BB22 {
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _50;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _50;
     [#"../hillel.rs" 171 4 171 58] _55 <- ([#"../hillel.rs" 171 4 171 58] Snapshot.new (Seq.(++) (Snapshot.inner produced1) (Seq.singleton __creusot_proc_iter_elem1)));
     goto BB23
   }
   BB23 {
     [#"../hillel.rs" 171 4 171 58] produced1 <- _55;
     _55 <- any Snapshot.snap_ty (Seq.seq usize);
-    [#"../../../../creusot-contracts-proc/src/lib.rs" 654 0 654 51] i <- __creusot_proc_iter_elem1;
+    [#"../../../../creusot-contracts-proc/src/lib.rs" 643 0 643 51] i <- __creusot_proc_iter_elem1;
     [#"../hillel.rs" 177 32 177 43] _60 <- total - sum;
     [#"../hillel.rs" 177 19 177 44] dist <- ([#"../hillel.rs" 177 19 177 44] abs_diff0 sum _60);
     _60 <- any uint32;

diff --git a/creusot/tests/should_succeed/iterators/01_range.mlcfg b/creusot/tests/should_succeed/iterators/01_range.mlcfg
@@ -339,57 +339,68 @@ module C01Range_SumRange
 end
 module C01Range_Impl0
   use prelude.IntSize
-  use seq.Seq
-  predicate invariant3 (self : Seq.seq isize) =
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  predicate invariant3 (self : Core_Option_Option_Type.t_option isize) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  val invariant3 (self : Seq.seq isize) : bool
+  val invariant3 (self : Core_Option_Option_Type.t_option isize) : bool
     ensures { result = invariant3 self }
 
-  predicate inv3 (_x : Seq.seq isize)
-  val inv3 (_x : Seq.seq isize) : bool
+  predicate inv3 (_x : Core_Option_Option_Type.t_option isize)
+  val inv3 (_x : Core_Option_Option_Type.t_option isize) : bool
     ensures { result = inv3 _x }
 
-  axiom inv3 : forall x : Seq.seq isize . inv3 x = true
+  axiom inv3 : forall x : Core_Option_Option_Type.t_option isize . inv3 x = true
   use C01Range_Range_Type as C01Range_Range_Type
-  predicate invariant2 (self : C01Range_Range_Type.t_range) =
+  use prelude.Borrow
+  predicate invariant2 (self : borrowed (C01Range_Range_Type.t_range)) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  val invariant2 (self : C01Range_Range_Type.t_range) : bool
+  val invariant2 (self : borrowed (C01Range_Range_Type.t_range)) : bool
     ensures { result = invariant2 self }
 
-  predicate inv2 (_x : C01Range_Range_Type.t_range)
-  val inv2 (_x : C01Range_Range_Type.t_range) : bool
+  predicate inv2 (_x : borrowed (C01Range_Range_Type.t_range))
+  val inv2 (_x : borrowed (C01Range_Range_Type.t_range)) : bool
     ensures { result = inv2 _x }
 
-  axiom inv2 : forall x : C01Range_Range_Type.t_range . inv2 x = true
-  use Core_Option_Option_Type as Core_Option_Option_Type
-  predicate invariant1 (self : Core_Option_Option_Type.t_option isize) =
+  axiom inv2 : forall x : borrowed (C01Range_Range_Type.t_range) . inv2 x = true
+  use seq.Seq
+  predicate invariant1 (self : Seq.seq isize) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  val invariant1 (self : Core_Option_Option_Type.t_option isize) : bool
+  val invariant1 (self : Seq.seq isize) : bool
     ensures { result = invariant1 self }
 
-  predicate inv1 (_x : Core_Option_Option_Type.t_option isize)
-  val inv1 (_x : Core_Option_Option_Type.t_option isize) : bool
+  predicate inv1 (_x : Seq.seq isize)
+  val inv1 (_x : Seq.seq isize) : bool
     ensures { result = inv1 _x }
 
-  axiom inv1 : forall x : Core_Option_Option_Type.t_option isize . inv1 x = true
-  use prelude.Borrow
-  predicate invariant0 (self : borrowed (C01Range_Range_Type.t_range)) =
+  axiom inv1 : forall x : Seq.seq isize . inv1 x = true
+  predicate invariant0 (self : C01Range_Range_Type.t_range) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  val invariant0 (self : borrowed (C01Range_Range_Type.t_range)) : bool
+  val invariant0 (self : C01Range_Range_Type.t_range) : bool
     ensures { result = invariant0 self }
 
-  predicate inv0 (_x : borrowed (C01Range_Range_Type.t_range))
-  val inv0 (_x : borrowed (C01Range_Range_Type.t_range)) : bool
+  predicate inv0 (_x : C01Range_Range_Type.t_range)
+  val inv0 (_x : C01Range_Range_Type.t_range) : bool
     ensures { result = inv0 _x }
 
-  axiom inv0 : forall x : borrowed (C01Range_Range_Type.t_range) . inv0 x = true
+  axiom inv0 : forall x : C01Range_Range_Type.t_range . inv0 x = true
   use seq.Seq
+  use prelude.Int
+  predicate resolve0 (self : borrowed (C01Range_Range_Type.t_range)) =
+    [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34]  ^ self =  * self
+  val resolve0 (self : borrowed (C01Range_Range_Type.t_range)) : bool
+    ensures { result = resolve0 self }
+
+  predicate completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) =
+    [#"../01_range.rs" 25 12 25 52] resolve0 self
+    /\ C01Range_Range_Type.range_start ( * self) >= C01Range_Range_Type.range_end ( * self)
+  val completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) : bool
+    ensures { result = completed0 self }
+
   use seq.Seq
   use seq.Seq
   use seq.Seq
   use prelude.IntSize
   use seq.Seq
-  use prelude.Int
   predicate produces0 [#"../01_range.rs" 31 4 31 64] (self : C01Range_Range_Type.t_range) (visited : Seq.seq isize) (o : C01Range_Range_Type.t_range)
 
    =
@@ -404,31 +415,20 @@ module C01Range_Impl0
     ensures { result = produces0 self visited o }
 
   use seq.Seq
-  predicate resolve0 (self : borrowed (C01Range_Range_Type.t_range)) =
-    [#"../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34]  ^ self =  * self
-  val resolve0 (self : borrowed (C01Range_Range_Type.t_range)) : bool
-    ensures { result = resolve0 self }
-
-  predicate completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) =
-    [#"../01_range.rs" 25 12 25 52] resolve0 self
-    /\ C01Range_Range_Type.range_start ( * self) >= C01Range_Range_Type.range_end ( * self)
-  val completed0 [#"../01_range.rs" 23 4 23 35] (self : borrowed (C01Range_Range_Type.t_range)) : bool
-    ensures { result = completed0 self }
-
-  goal next_refn : [#"../01_range.rs" 57 4 57 39] forall self : borrowed (C01Range_Range_Type.t_range) . inv0 self
+  goal produces_refl_refn : [#"../01_range.rs" 44 4 44 26] forall self : C01Range_Range_Type.t_range . inv0 self
+   -> (forall result : () . produces0 self (Seq.empty ) self  -> produces0 self (Seq.empty ) self)
+  goal produces_trans_refn : [#"../01_range.rs" 51 4 51 90] forall a : C01Range_Range_Type.t_range . forall ab : Seq.seq isize . forall b : C01Range_Range_Type.t_range . forall bc : Seq.seq isize . forall c : C01Range_Range_Type.t_range . inv0 c
+  /\ inv1 bc /\ inv0 b /\ inv1 ab /\ inv0 a /\ produces0 b bc c /\ produces0 a ab b
+   -> produces0 b bc c
+  /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c  -> produces0 a (Seq.(++) ab bc) c)
+  goal next_refn : [#"../01_range.rs" 57 4 57 39] forall self : borrowed (C01Range_Range_Type.t_range) . inv2 self
    -> (forall result : Core_Option_Option_Type.t_option isize . match result with
     | Core_Option_Option_Type.C_None -> completed0 self
     | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self)
     end
-   -> inv1 result
+   -> inv3 result
   /\ match result with
     | Core_Option_Option_Type.C_None -> completed0 self
     | Core_Option_Option_Type.C_Some v -> produces0 ( * self) (Seq.singleton v) ( ^ self)
     end)
-  goal produces_trans_refn : [#"../01_range.rs" 51 4 51 90] forall a : C01Range_Range_Type.t_range . forall ab : Seq.seq isize . forall b : C01Range_Range_Type.t_range . forall bc : Seq.seq isize . forall c : C01Range_Range_Type.t_range . inv2 c
-  /\ inv3 bc /\ inv2 b /\ inv3 ab /\ inv2 a /\ produces0 b bc c /\ produces0 a ab b
-   -> produces0 b bc c
-  /\ produces0 a ab b /\ (forall result : () . produces0 a (Seq.(++) ab bc) c  -> produces0 a (Seq.(++) ab bc) c)
-  goal produces_refl_refn : [#"../01_range.rs" 44 4 44 26] forall self : C01Range_Range_Type.t_range . inv2 self
-   -> (forall result : () . produces0 self (Seq.empty ) self  -> produces0 self (Seq.empty ) self)
 end
diff --git a/creusot/tests/should_succeed/iterators/01_range/why3session.xml b/creusot/tests/should_succeed/iterators/01_range/why3session.xml
@@ -31,14 +31,14 @@
  </goal>
 </theory>
 <theory name="C01Range_Impl0" proved="true">
- <goal name="next_refn" proved="true">
- <proof prover="0"><result status="valid" time="0.013215" steps="112"/></proof>
+ <goal name="produces_refl_refn" proved="true">
+ <proof prover="0"><result status="valid" time="0.016725" steps="0"/></proof>
  </goal>
  <goal name="produces_trans_refn" proved="true">
  <proof prover="0"><result status="valid" time="0.013647" steps="14"/></proof>
  </goal>
- <goal name="produces_refl_refn" proved="true">
- <proof prover="0"><result status="valid" time="0.016725" steps="0"/></proof>
+ <goal name="next_refn" proved="true">
+ <proof prover="0"><result status="valid" time="0.013215" steps="112"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz b/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz