Update test proofs

creusot-rs · Jan 29, 2024 · 312ccd8 · 312ccd8
1 parent 2066c8a
commit 312ccd8
Show file tree

Hide file tree

Showing 255 changed files with 3,866 additions and 3,879 deletions.
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
@@ -697,7 +697,7 @@ impl<'tcx> Statement<'tcx> {
                     place::create_assign_inner(ctx, names, locals, &rhs, reassign, span),
                 ]
             }
-            Statement::Assignment(lhs, RValue::FinalBorrow(rhs, deref_index)) => {
+            Statement::Assignment(lhs, RValue::FinalBorrow(rhs, deref_index), span) => {
                 let original_borrow = Place {
                     local: rhs.local.clone(),
                     projection: rhs.projection[..deref_index].to_vec(),
@@ -712,8 +712,8 @@ impl<'tcx> Statement<'tcx> {
                 let reassign = Exp::Final(Box::new(lhs.as_rplace(ctx, names, locals)));
 
                 vec![
-                    place::create_assign_inner(ctx, names, locals, &lhs, borrow),
-                    place::create_assign_inner(ctx, names, locals, &rhs, reassign),
+                    place::create_assign_inner(ctx, names, locals, &lhs, borrow, span),
+                    place::create_assign_inner(ctx, names, locals, &rhs, reassign, span),
                 ]
             }
             Statement::Assignment(lhs, RValue::Ghost(rhs), span) => {

diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
@@ -257,11 +257,11 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             }
             TermKind::Absurd => Exp::Absurd,
             TermKind::Reborrow { cur, fin, term, projection } => {
-                let inner = self.lower_term(*term);
+                let inner = self.lower_term(&*term);
                 let borrow_id = borrow_generated_id(inner, &projection);
                 Exp::Call(
                     Box::new(Exp::QVar("Borrow.borrow_logic".into(), Purity::Logic)),
-                    vec![self.lower_term(*cur), self.lower_term(*fin), borrow_id],
+                    vec![self.lower_term(&*cur), self.lower_term(&*fin), borrow_id],
                 )
             }
             TermKind::Assert { cond } => {

diff --git a/creusot/tests/should_fail/bug/222.mlcfg b/creusot/tests/should_fail/bug/222.mlcfg
@@ -93,8 +93,8 @@ module C222_UsesInvariant
     goto BB0
   }
   BB0 {
-    [#"../222.rs" 41 4 41 14] _5 <- Borrow.borrow_mut (C222_Once_Type.once_0 ( * x));
-    [#"../222.rs" 41 4 41 14] x <- { x with current = (let C222_Once_Type.C_Once x0 =  * x in C222_Once_Type.C_Once ( ^ _5)) };
+    [#"../222.rs" 41 4 41 14] _5 <- Borrow.borrow_final (C222_Once_Type.once_0 ( * x)) (Borrow.inherit_id (Borrow.get_id x) 1);
+    [#"../222.rs" 41 4 41 14] x <- { x with current = (let C222_Once_Type.C_Once x0 =  * x in C222_Once_Type.C_Once ( ^ _5)) ; };
     assume { inv0 ( ^ _5) };
     [#"../222.rs" 41 4 41 14] _4 <- ([#"../222.rs" 41 4 41 14] take0 _5);
     _5 <- any borrowed (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
@@ -49,8 +49,8 @@ module C492_ReborrowTuple
     goto BB0
   }
   BB0 {
-    [#"../492.rs" 6 5 6 6] _3 <- Borrow.borrow_mut ( * x);
-    [#"../492.rs" 6 5 6 6] x <- { x with current =  ^ _3 };
+    [#"../492.rs" 6 5 6 6] _3 <- Borrow.borrow_final ( * x) (Borrow.get_id x);
+    [#"../492.rs" 6 5 6 6] x <- { x with current = ( ^ _3) ; };
     assume { inv0 ( ^ _3) };
     [#"../492.rs" 6 4 6 11] _0 <- ([#"../492.rs" 6 4 6 11] (_3, ([#"../492.rs" 6 8 6 10] [#"../492.rs" 6 8 6 10] (32 : uint32))));
     _3 <- any borrowed t;
@@ -122,8 +122,8 @@ module C492_Test
     [#"../492.rs" 11 16 11 17] x <- ([#"../492.rs" 11 16 11 17] [#"../492.rs" 11 16 11 17] (5 : int32));
     [#"../492.rs" 12 34 12 40] _6 <- Borrow.borrow_mut x;
     [#"../492.rs" 12 34 12 40] x <-  ^ _6;
-    [#"../492.rs" 12 34 12 40] _5 <- Borrow.borrow_mut ( * _6);
-    [#"../492.rs" 12 34 12 40] _6 <- { _6 with current =  ^ _5 };
+    [#"../492.rs" 12 34 12 40] _5 <- Borrow.borrow_final ( * _6) (Borrow.get_id _6);
+    [#"../492.rs" 12 34 12 40] _6 <- { _6 with current = ( ^ _5) ; };
     [#"../492.rs" 12 19 12 41] _4 <- ([#"../492.rs" 12 19 12 41] reborrow_tuple0 _5);
     _5 <- any borrowed int32;
     goto BB1
@@ -134,7 +134,7 @@ module C492_Test
     assume { resolve0 _4 };
     assume { resolve1 _6 };
     assert { [@expl:assertion] [#"../492.rs" 13 18 13 30]  ^ res = (5 : int32) };
-    [#"../492.rs" 14 4 14 13] res <- { res with current = ([#"../492.rs" 14 4 14 13] [#"../492.rs" 14 11 14 13] (10 : int32)) };
+    [#"../492.rs" 14 4 14 13] res <- { res with current = ([#"../492.rs" 14 4 14 13] [#"../492.rs" 14 11 14 13] (10 : int32)) ; };
     assume { resolve1 res };
     [#"../492.rs" 10 14 15 1] _0 <- ([#"../492.rs" 10 14 15 1] ());
     return _0

diff --git a/creusot/tests/should_fail/bug/692.mlcfg b/creusot/tests/should_fail/bug/692.mlcfg
@@ -227,7 +227,7 @@ module C692_ValidNormal_Closure2
     goto BB3
   }
   BB3 {
-    [#"../692.rs" 16 14 16 39] _1 <- { _1 with current = (let C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 x0 =  * _1 in C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 ({ (field_00 ( * _1)) with current = ([#"../692.rs" 16 14 16 39] _4) })) };
+    [#"../692.rs" 16 14 16 39] _1 <- { _1 with current = (let C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 x0 =  * _1 in C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 ({ (field_00 ( * _1)) with current = ([#"../692.rs" 16 14 16 39] _4) ; })) ; };
     [#"../692.rs" 16 14 16 39] _4 <- any uint32;
     assume { resolve0 _1 };
     [#"../692.rs" 16 14 16 39] res <- ([#"../692.rs" 16 14 16 39] ());

diff --git a/creusot/tests/should_fail/bug/695.mlcfg b/creusot/tests/should_fail/bug/695.mlcfg
@@ -285,7 +285,7 @@ module C695_Valid_Closure2
     goto BB3
   }
   BB3 {
-    [#"../695.rs" 20 14 20 39] _1 <- { _1 with current = (let C695_Valid_Closure2.C695_Valid_Closure2 x0 =  * _1 in C695_Valid_Closure2.C695_Valid_Closure2 ({ (field_00 ( * _1)) with current = ([#"../695.rs" 20 14 20 39] _4) })) };
+    [#"../695.rs" 20 14 20 39] _1 <- { _1 with current = (let C695_Valid_Closure2.C695_Valid_Closure2 x0 =  * _1 in C695_Valid_Closure2.C695_Valid_Closure2 ({ (field_00 ( * _1)) with current = ([#"../695.rs" 20 14 20 39] _4) ; })) ; };
     [#"../695.rs" 20 14 20 39] _4 <- any uint32;
     assume { resolve0 _1 };
     [#"../695.rs" 20 14 20 39] res <- ([#"../695.rs" 20 14 20 39] ());

diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
@@ -405,8 +405,8 @@ module C100doors_F
   BB7 {
     [#"../100doors.rs" 20 4 20 41] _14 <- Borrow.borrow_mut iter;
     [#"../100doors.rs" 20 4 20 41] iter <-  ^ _14;
-    [#"../100doors.rs" 20 4 20 41] _13 <- Borrow.borrow_mut ( * _14);
-    [#"../100doors.rs" 20 4 20 41] _14 <- { _14 with current =  ^ _13 };
+    [#"../100doors.rs" 20 4 20 41] _13 <- Borrow.borrow_final ( * _14) (Borrow.get_id _14);
+    [#"../100doors.rs" 20 4 20 41] _14 <- { _14 with current = ( ^ _13) ; };
     [#"../100doors.rs" 20 4 20 41] _12 <- ([#"../100doors.rs" 20 4 20 41] next0 _13);
     _13 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize);
     goto BB8
@@ -469,7 +469,7 @@ module C100doors_F
     goto BB19
   }
   BB19 {
-    [#"../100doors.rs" 26 12 26 54] _30 <- { _30 with current = ([#"../100doors.rs" 26 12 26 54] not ([#"../100doors.rs" 26 35 26 54] _26)) };
+    [#"../100doors.rs" 26 12 26 54] _30 <- { _30 with current = ([#"../100doors.rs" 26 12 26 54] not ([#"../100doors.rs" 26 35 26 54] _26)) ; };
     assume { resolve1 _30 };
     [#"../100doors.rs" 27 12 27 24] door <- ([#"../100doors.rs" 27 12 27 24] door + ([#"../100doors.rs" 27 20 27 24] pass));
     [#"../100doors.rs" 25 26 28 9] _11 <- ([#"../100doors.rs" 25 26 28 9] ());

diff --git a/creusot/tests/should_succeed/100doors/why3session.xml b/creusot/tests/should_succeed/100doors/why3session.xml
@@ -7,7 +7,7 @@
 <path name=".."/><path name="100doors.mlcfg"/>
 <theory name="C100doors_F" proved="true">
  <goal name="f&#39;vc" expl="VC for f" proved="true">
- <proof prover="1"><result status="valid" time="0.122415" steps="757939"/></proof>
+ <proof prover="1"><result status="valid" time="0.122415" steps="677037"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_succeed/100doors/why3shapes.gz b/creusot/tests/should_succeed/100doors/why3shapes.gz
diff --git a/creusot/tests/should_succeed/all_zero.mlcfg b/creusot/tests/should_succeed/all_zero.mlcfg
@@ -104,14 +104,14 @@ module AllZero_AllZero
     goto BB5
   }
   BB5 {
-    [#"../all_zero.rs" 43 19 43 24] value <- Borrow.borrow_mut (AllZero_List_Type.cons_0 ( * loop_l));
-    [#"../all_zero.rs" 43 19 43 24] loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons x0 x1 =  * loop_l in AllZero_List_Type.C_Cons ( ^ value) x1) };
-    [#"../all_zero.rs" 43 26 43 30] next <- Borrow.borrow_mut (AllZero_List_Type.cons_1 ( * loop_l));
-    [#"../all_zero.rs" 43 26 43 30] loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons x0 x1 =  * loop_l in AllZero_List_Type.C_Cons x0 ( ^ next)) };
-    [#"../all_zero.rs" 44 8 44 18] value <- { value with current = ([#"../all_zero.rs" 44 8 44 18] [#"../all_zero.rs" 44 17 44 18] (0 : uint32)) };
+    [#"../all_zero.rs" 43 19 43 24] value <- Borrow.borrow_final (AllZero_List_Type.cons_0 ( * loop_l)) (Borrow.inherit_id (Borrow.get_id loop_l) 1);
+    [#"../all_zero.rs" 43 19 43 24] loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons x0 x1 =  * loop_l in AllZero_List_Type.C_Cons ( ^ value) x1) ; };
+    [#"../all_zero.rs" 43 26 43 30] next <- Borrow.borrow_final (AllZero_List_Type.cons_1 ( * loop_l)) (Borrow.inherit_id (Borrow.get_id loop_l) 2);
+    [#"../all_zero.rs" 43 26 43 30] loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons x0 x1 =  * loop_l in AllZero_List_Type.C_Cons x0 ( ^ next)) ; };
+    [#"../all_zero.rs" 44 8 44 18] value <- { value with current = ([#"../all_zero.rs" 44 8 44 18] [#"../all_zero.rs" 44 17 44 18] (0 : uint32)) ; };
     assume { resolve0 value };
     [#"../all_zero.rs" 45 17 45 21] _13 <- Borrow.borrow_mut ( * next);
-    [#"../all_zero.rs" 45 17 45 21] next <- { next with current =  ^ _13 };
+    [#"../all_zero.rs" 45 17 45 21] next <- { next with current = ( ^ _13) ; };
     assume { resolve1 loop_l };
     [#"../all_zero.rs" 45 8 45 21] loop_l <- ([#"../all_zero.rs" 45 8 45 21] _13);
     [#"../all_zero.rs" 45 8 45 21] _13 <- any borrowed (AllZero_List_Type.t_list);

diff --git a/creusot/tests/should_succeed/all_zero/why3session.xml b/creusot/tests/should_succeed/all_zero/why3session.xml
@@ -7,7 +7,7 @@
 <path name=".."/><path name="all_zero.mlcfg"/>
 <theory name="AllZero_AllZero" proved="true">
  <goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
- <proof prover="0"><result status="valid" time="0.038573" steps="805"/></proof>
+ <proof prover="0"><result status="valid" time="0.038573" steps="893"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_succeed/all_zero/why3shapes.gz b/creusot/tests/should_succeed/all_zero/why3shapes.gz