Update tests

creusot-rs · Jan 3, 2024 · b46a8f3 · b46a8f3
1 parent 26e2da1
commit b46a8f3
Show file tree

Hide file tree

Showing 344 changed files with 4,854 additions and 3,293 deletions.
diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg b/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg
@@ -94,11 +94,11 @@ module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface
   function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
   val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
     requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Int.le (Seq.length result) (UIntSize.to_int Max0.mAX') }
     ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
     ensures { result = shallow_model self }
 
-  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Int.le (Seq.length (shallow_model self)) (UIntSize.to_int Max0.mAX'))
 end
 module CreusotContracts_Std1_Vec_Impl0_ShallowModel
   type t
@@ -116,11 +116,11 @@ module CreusotContracts_Std1_Vec_Impl0_ShallowModel
   function shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
   val shallow_model (self : Alloc_Vec_Vec_Type.t_vec t a) : Seq.seq t
     requires {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Int.le (Seq.length result) (UIntSize.to_int Max0.mAX') }
     ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv result }
     ensures { result = shallow_model self }
 
-  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+  axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Int.le (Seq.length (shallow_model self)) (UIntSize.to_int Max0.mAX'))
 end
 module Alloc_Alloc_Global_Type
   type t_global  =
@@ -130,6 +130,7 @@ end
 module Alloc_Vec_Impl0_New_Interface
   type t
   use seq.Seq
+  use prelude.Int
   use seq.Seq
   clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
     type t = Seq.seq t
@@ -214,6 +215,7 @@ module Alloc_Vec_Impl1_Push_Interface
   type a
   use prelude.Borrow
   use seq.Seq
+  use prelude.Bool
   use seq.Seq
   clone CreusotContracts_Invariant_Inv_Stub as Inv3 with
     type t = Seq.seq t
@@ -273,6 +275,7 @@ end
 module C01ResolveUnsoundness_MakeVecOfSize
   use prelude.Int
   use prelude.UIntSize
+  use prelude.Bool
   use prelude.Borrow
   use seq.Seq
   clone CreusotContracts_Invariant_Inv_Interface as Inv3 with
@@ -352,11 +355,11 @@ module C01ResolveUnsoundness_MakeVecOfSize
     goto BB2
   }
   BB2 {
-    invariant { [#"../01_resolve_unsoundness.rs" 12 16 12 37] (0 : usize) <= i /\ i <= n };
+    invariant { [#"../01_resolve_unsoundness.rs" 12 16 12 37] Int.le (0 : usize) i /\ Int.le i n };
     goto BB3
   }
   BB3 {
-    switch ([#"../01_resolve_unsoundness.rs" 13 10 13 16] i <= n)
+    switch ([#"../01_resolve_unsoundness.rs" 13 10 13 16] UIntSize.le i n)
       | False -> goto BB6
       | True -> goto BB4
       end
@@ -369,7 +372,7 @@ module C01ResolveUnsoundness_MakeVecOfSize
     goto BB5
   }
   BB5 {
-    i <- ([#"../01_resolve_unsoundness.rs" 15 8 15 14] i + ([#"../01_resolve_unsoundness.rs" 15 13 15 14] [#"../01_resolve_unsoundness.rs" 15 13 15 14] (1 : usize)));
+    i <- ([#"../01_resolve_unsoundness.rs" 15 8 15 14] UIntSize.add i ([#"../01_resolve_unsoundness.rs" 15 13 15 14] [#"../01_resolve_unsoundness.rs" 15 13 15 14] (1 : usize)));
     goto BB2
   }
   BB6 {

diff --git a/creusot/tests/should_fail/bug/222.mlcfg b/creusot/tests/should_fail/bug/222.mlcfg
@@ -35,10 +35,10 @@ module C222_A_IsTrue_Interface
     type self = self
   function is_true [#"../222.rs" 14 4 14 16] (_1 : ()) : ()
   val is_true [#"../222.rs" 14 4 14 16] (_1 : ()) : ()
-    ensures { [#"../222.rs" 13 14 13 34] Mktrue0.mktrue () <= 10 }
+    ensures { [#"../222.rs" 13 14 13 34] Int.le (Mktrue0.mktrue ()) 10 }
     ensures { result = is_true _1 }
 
-  axiom is_true_spec : forall _1 : () . [#"../222.rs" 13 14 13 34] Mktrue0.mktrue () <= 10
+  axiom is_true_spec : forall _1 : () . [#"../222.rs" 13 14 13 34] Int.le (Mktrue0.mktrue ()) 10
 end
 module C222_A_IsTrue
   type self
@@ -48,18 +48,18 @@ module C222_A_IsTrue
   function is_true [#"../222.rs" 14 4 14 16] (_1 : ()) : () =
     [#"../222.rs" 15 8 15 10] ()
   val is_true [#"../222.rs" 14 4 14 16] (_1 : ()) : ()
-    ensures { [#"../222.rs" 13 14 13 34] Mktrue0.mktrue () <= 10 }
+    ensures { [#"../222.rs" 13 14 13 34] Int.le (Mktrue0.mktrue ()) 10 }
     ensures { result = is_true _1 }
 
-  axiom is_true_spec : forall _1 : () . [#"../222.rs" 13 14 13 34] Mktrue0.mktrue () <= 10
+  axiom is_true_spec : forall _1 : () . [#"../222.rs" 13 14 13 34] Int.le (Mktrue0.mktrue ()) 10
 end
 module C222_A_IsTrue_Impl
   type self
   use prelude.Int
   clone C222_A_Mktrue_Interface as Mktrue0 with
     type self = self
   let rec ghost function is_true [#"../222.rs" 14 4 14 16] (_1 : ()) : ()
-    ensures { [#"../222.rs" 13 14 13 34] Mktrue0.mktrue () <= 10 }
+    ensures { [#"../222.rs" 13 14 13 34] Int.le (Mktrue0.mktrue ()) 10 }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
     [#"../222.rs" 15 8 15 10] ()
@@ -171,6 +171,7 @@ end
 module CreusotContracts_Resolve_Impl1_Resolve
   type t
   use prelude.Borrow
+  use prelude.Bool
   predicate resolve (self : borrowed t) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34]  ^ self =  * self
   val resolve (self : borrowed t) : bool
@@ -186,6 +187,7 @@ end
 module Core_Option_Impl0_Take_Interface
   type t
   use prelude.Borrow
+  use prelude.Bool
   use Core_Option_Option_Type as Core_Option_Option_Type
   clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
     type t = Core_Option_Option_Type.t_option t

diff --git a/creusot/tests/should_fail/bug/492.mlcfg b/creusot/tests/should_fail/bug/492.mlcfg
@@ -34,6 +34,7 @@ end
 module CreusotContracts_Resolve_Impl1_Resolve
   type t
   use prelude.Borrow
+  use prelude.Bool
   predicate resolve (self : borrowed t) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34]  ^ self =  * self
   val resolve (self : borrowed t) : bool
@@ -49,6 +50,7 @@ end
 module C492_ReborrowTuple_Interface
   type t
   use prelude.Borrow
+  use prelude.Bool
   use prelude.Int
   use prelude.UInt32
   clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
@@ -66,6 +68,7 @@ module C492_ReborrowTuple
   use prelude.Int
   use prelude.UInt32
   use prelude.Borrow
+  use prelude.Bool
   clone CreusotContracts_Invariant_Inv_Interface as Inv2 with
     type t = (borrowed t, uint32)
   clone TyInv_Trivial as TyInv_Trivial2 with
@@ -144,6 +147,7 @@ end
 module CreusotContracts_Resolve_Impl0_Resolve
   type t1
   type t2
+  use prelude.Bool
   clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve1 with
     type self = t2
   clone CreusotContracts_Resolve_Resolve_Resolve_Stub as Resolve0 with

diff --git a/creusot/tests/should_fail/bug/692.mlcfg b/creusot/tests/should_fail/bug/692.mlcfg
@@ -150,6 +150,7 @@ end
 module CreusotContracts_Resolve_Impl1_Resolve
   type t
   use prelude.Borrow
+  use prelude.Bool
   predicate resolve (self : borrowed t) =
     [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34]  ^ self =  * self
   val resolve (self : borrowed t) : bool
@@ -160,6 +161,7 @@ module CreusotContracts_Std1_Ops_Impl2_FnMut_Stub
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -185,6 +187,7 @@ module CreusotContracts_Std1_Ops_Impl2_FnMut_Interface
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -218,6 +221,7 @@ module CreusotContracts_Std1_Ops_Impl2_FnMut
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -280,6 +284,7 @@ end
 module CreusotContracts_Std1_Ops_Impl2_FnOnce_Stub
   type args
   type f
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -304,6 +309,7 @@ end
 module CreusotContracts_Std1_Ops_Impl2_FnOnce_Interface
   type args
   type f
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -336,6 +342,7 @@ end
 module CreusotContracts_Std1_Ops_Impl2_FnOnce
   type args
   type f
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -569,6 +576,7 @@ module CreusotContracts_Std1_Ops_Impl1_FnMutOnce_Stub
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -596,6 +604,7 @@ module CreusotContracts_Std1_Ops_Impl1_FnMutOnce_Interface
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -631,6 +640,7 @@ module CreusotContracts_Std1_Ops_Impl1_FnMutOnce
   type args
   type f
   use prelude.Borrow
+  use prelude.Bool
   clone Core_Ops_Function_FnOnce_Output_Type as Output0 with
     type self = f,
     type args = args
@@ -665,6 +675,7 @@ end
 module C692_Incorrect_Interface
   type c
   type b
+  use prelude.Bool
   clone CreusotContracts_Invariant_Inv_Stub as Inv1 with
     type t = b
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
@@ -689,6 +700,7 @@ end
 module C692_Incorrect
   type c
   type b
+  use prelude.Bool
   use prelude.Borrow
   clone CreusotContracts_Std1_Ops_Impl1_Unnest_Interface as Unnest0 with
     type args = (),
@@ -867,6 +879,7 @@ module C692_ValidNormal_Closure2_Interface
   use prelude.Borrow
   use prelude.Int
   use prelude.UInt32
+  use prelude.Bool
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = uint32
   let function field_0 [#"../692.rs" 15 17 15 64] (self : c692_validnormal_closure2) : borrowed uint32
@@ -895,6 +908,7 @@ module C692_ValidNormal_Closure2
   use prelude.Int
   use prelude.UInt32
   use prelude.Borrow
+  use prelude.Bool
   clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with
     type t = uint32
   clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with
@@ -963,6 +977,7 @@ module C692_ValidNormal_Closure1_Interface
   use export C692_ValidNormal_Closure1_Type
   use prelude.Int
   use prelude.UInt32
+  use prelude.Bool
   use prelude.Borrow
   let function field_0 [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) : uint32
    = [@vc:do_not_keep_trace] [@vc:sp]
@@ -974,22 +989,23 @@ module C692_ValidNormal_Closure1_Interface
   predicate precondition [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) =
     [#"../692.rs" 1 0 1 0] true
   predicate postcondition_once [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) (result : bool) =
-    [#"../692.rs" 13 25 13 45] result = (field_0 self > (7 : uint32))
+    [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 self) (7 : uint32)
   predicate postcondition_mut [#"../692.rs" 13 15 13 47] (self : borrowed c692_validnormal_closure1) (_ : ()) (result : bool)
 
    =
-    [#"../692.rs" 1 0 1 0] result = (field_0 ( ^ self) > (7 : uint32)) /\ unnest ( * self) ( ^ self)
+    [#"../692.rs" 1 0 1 0] result = Int.gt (field_0 ( ^ self)) (7 : uint32) /\ unnest ( * self) ( ^ self)
   predicate postcondition [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) (result : bool) =
-    [#"../692.rs" 13 25 13 45] result = (field_0 self > (7 : uint32))
+    [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 self) (7 : uint32)
   val c692_ValidNormal_Closure1 [#"../692.rs" 13 15 13 47] (_1 : c692_validnormal_closure1) : bool
-    ensures { [#"../692.rs" 13 25 13 45] result = (field_0 _1 > (7 : uint32)) }
+    ensures { [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 _1) (7 : uint32) }
 
 end
 module C692_ValidNormal_Closure1
   use export C692_ValidNormal_Closure1_Type
   use prelude.Int
   use prelude.UInt32
   use prelude.Borrow
+  use prelude.Bool
   let function field_0 [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) : uint32
    = [@vc:do_not_keep_trace] [@vc:sp]
     [#"../692.rs" 1 0 1 0] let C692_ValidNormal_Closure1 a = self in a
@@ -1000,15 +1016,15 @@ module C692_ValidNormal_Closure1
   predicate precondition [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) =
     [#"../692.rs" 1 0 1 0] true
   predicate postcondition_once [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) (result : bool) =
-    [#"../692.rs" 13 25 13 45] result = (field_0 self > (7 : uint32))
+    [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 self) (7 : uint32)
   predicate postcondition_mut [#"../692.rs" 13 15 13 47] (self : borrowed c692_validnormal_closure1) (_ : ()) (result : bool)
 
    =
-    [#"../692.rs" 1 0 1 0] result = (field_0 ( ^ self) > (7 : uint32)) /\ unnest ( * self) ( ^ self)
+    [#"../692.rs" 1 0 1 0] result = Int.gt (field_0 ( ^ self)) (7 : uint32) /\ unnest ( * self) ( ^ self)
   predicate postcondition [#"../692.rs" 13 15 13 47] (self : c692_validnormal_closure1) (_ : ()) (result : bool) =
-    [#"../692.rs" 13 25 13 45] result = (field_0 self > (7 : uint32))
+    [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 self) (7 : uint32)
   let rec cfg c692_ValidNormal_Closure1 [#"../692.rs" 13 15 13 47] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : c692_validnormal_closure1) : bool
-    ensures { [#"../692.rs" 13 25 13 45] result = (field_0 _1 > (7 : uint32)) }
+    ensures { [#"../692.rs" 13 25 13 45] result = Int.gt (field_0 _1) (7 : uint32) }
 
    = [@vc:do_not_keep_trace] [@vc:sp]
   var _0 : bool;
@@ -1018,7 +1034,7 @@ module C692_ValidNormal_Closure1
     goto BB0
   }
   BB0 {
-    res <- ([#"../692.rs" 14 7 14 15] field_0 _1 > ([#"../692.rs" 14 11 14 15] [#"../692.rs" 14 11 14 15] (7 : uint32)));
+    res <- ([#"../692.rs" 14 7 14 15] UInt32.gt (field_0 _1) ([#"../692.rs" 14 11 14 15] [#"../692.rs" 14 11 14 15] (7 : uint32)));
     _0 <- res;
     return _0
   }