Change some tests to pass with final borrows

creusot/tests/should_succeed/100doors.mlcfg

@@ -1357,7 +1357,7 @@ module C100doors_F
   BB7 {
     _14 <- Borrow.borrow_mut iter;
     iter <-  ^ _14;
-    _13 <- Borrow.borrow_mut ( * _14);
+    _13 <- Borrow.borrow_final ( * _14) (Borrow.get_id _14);
     _14 <- { _14 with current = ( ^ _13) ; };
     _12 <- ([#"../100doors.rs" 20 4 20 41] Next0.next _13);
     _13 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize);

creusot/tests/should_succeed/all_zero.mlcfg

@@ -172,9 +172,9 @@ module AllZero_AllZero
     goto BB5
   }
   BB5 {
-    value <- Borrow.borrow_mut (AllZero_List_Type.cons_0 ( * loop_l));
+    value <- Borrow.borrow_final (AllZero_List_Type.cons_0 ( * loop_l)) (Borrow.inherit_id (Borrow.get_id loop_l) 1);
     loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons ( ^ value) b) ; };
-    next <- Borrow.borrow_mut (AllZero_List_Type.cons_1 ( * loop_l));
+    next <- Borrow.borrow_final (AllZero_List_Type.cons_1 ( * loop_l)) (Borrow.inherit_id (Borrow.get_id loop_l) 2);
     loop_l <- { loop_l with current = (let AllZero_List_Type.C_Cons a b =  * loop_l in AllZero_List_Type.C_Cons a ( ^ next)) ; };
     value <- { value with current = ([#"../all_zero.rs" 44 17 44 18] (0 : uint32)) ; };
     assume { Resolve0.resolve value };

creusot/tests/should_succeed/bdd.mlcfg

@@ -3023,7 +3023,7 @@ module Bdd_Impl11_Hashcons
   BB5 {
     r1 <- Bdd_Bdd_Type.C_Bdd ( * _19) (Bdd_Context_Type.context_cnt ( * self));
     assume { Resolve1.resolve _19 };
-    _24 <- Borrow.borrow_mut (Bdd_Context_Type.context_hashcons ( * self));
+    _24 <- Borrow.borrow_final (Bdd_Context_Type.context_hashcons ( * self)) (Borrow.inherit_id (Borrow.get_id self) 2);
     self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a ( ^ _24) c d e f) ; };
     _23 <- ([#"../bdd.rs" 446 8 446 31] Add0.add _24 n r1);
     _24 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Node_Type.t_node) (Bdd_Bdd_Type.t_bdd));
@@ -3220,7 +3220,7 @@ module Bdd_Impl11_Node
     goto BB5
   }
   BB3 {
-    _17 <- Borrow.borrow_mut ( * self);
+    _17 <- Borrow.borrow_final ( * self) (Borrow.get_id self);
     self <- { self with current = ( ^ _17) ; };
     assume { Inv0.inv ( ^ _17) };
     _0 <- ([#"../bdd.rs" 469 8 469 50] Hashcons0.hashcons _17 (Bdd_Node_Type.C_If x childt childf));
@@ -3352,7 +3352,7 @@ module Bdd_Impl11_True
     goto BB0
   }
   BB0 {
-    _6 <- Borrow.borrow_mut ( * self);
+    _6 <- Borrow.borrow_final ( * self) (Borrow.get_id self);
     self <- { self with current = ( ^ _6) ; };
     assume { Inv0.inv ( ^ _6) };
     _0 <- ([#"../bdd.rs" 477 8 477 27] Hashcons0.hashcons _6 (Bdd_Node_Type.C_True));
@@ -3481,7 +3481,7 @@ module Bdd_Impl11_False
     goto BB0
   }
   BB0 {
-    _6 <- Borrow.borrow_mut ( * self);
+    _6 <- Borrow.borrow_final ( * self) (Borrow.get_id self);
     self <- { self with current = ( ^ _6) ; };
     assume { Inv0.inv ( ^ _6) };
     _0 <- ([#"../bdd.rs" 485 8 485 28] Hashcons0.hashcons _6 (Bdd_Node_Type.C_False));
@@ -3642,7 +3642,7 @@ module Bdd_Impl11_V
     goto BB2
   }
   BB2 {
-    _10 <- Borrow.borrow_mut ( * self);
+    _10 <- Borrow.borrow_final ( * self) (Borrow.get_id self);
     self <- { self with current = ( ^ _10) ; };
     assume { Inv0.inv ( ^ _10) };
     _0 <- ([#"../bdd.rs" 494 8 494 26] Node0.node _10 x t f);
@@ -3955,7 +3955,7 @@ module Bdd_Impl11_Not
     goto BB16
   }
   BB16 {
-    _35 <- Borrow.borrow_mut (Bdd_Context_Type.context_not_memo ( * self));
+    _35 <- Borrow.borrow_final (Bdd_Context_Type.context_not_memo ( * self)) (Borrow.inherit_id (Borrow.get_id self) 4);
     self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c ( ^ _35) e f) ; };
     _34 <- ([#"../bdd.rs" 516 8 516 31] Add0.add _35 x r1);
     _35 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Bdd_Type.t_bdd) (Bdd_Bdd_Type.t_bdd));
@@ -4657,7 +4657,7 @@ module Bdd_Impl11_And
     goto BB33
   }
   BB33 {
-    _79 <- Borrow.borrow_mut (Bdd_Context_Type.context_and_memo ( * self));
+    _79 <- Borrow.borrow_final (Bdd_Context_Type.context_and_memo ( * self)) (Borrow.inherit_id (Borrow.get_id self) 5);
     self <- { self with current = (let Bdd_Context_Type.C_Context a b c d e f =  * self in Bdd_Context_Type.C_Context a b c d ( ^ _79) f) ; };
     _78 <- ([#"../bdd.rs" 560 8 560 36] Add0.add _79 (a, b) r1);
     _79 <- any borrowed (Bdd_Hashmap_MyHashMap_Type.t_myhashmap (Bdd_Bdd_Type.t_bdd, Bdd_Bdd_Type.t_bdd) (Bdd_Bdd_Type.t_bdd));

creusot/tests/should_succeed/bug/682.mlcfg

@@ -104,7 +104,7 @@ module C682_Foo
     goto BB1
   }
   BB1 {
-    _7 <- Borrow.borrow_mut ( * a);
+    _7 <- Borrow.borrow_final ( * a) (Borrow.get_id a);
     a <- { a with current = ( ^ _7) ; };
     _6 <- ([#"../682.rs" 14 4 14 15] AddSome0.add_some _7);
     _7 <- any borrowed uint64;

creusot/tests/should_succeed/bug/766.mlcfg

@@ -189,7 +189,7 @@ module C766_Trait_Goo
     goto BB0
   }
   BB0 {
-    _2 <- Borrow.borrow_mut ( * self);
+    _2 <- Borrow.borrow_final ( * self) (Borrow.get_id self);
     self <- { self with current = ( ^ _2) ; };
     assume { Inv0.inv ( ^ _2) };
     _0 <- ([#"../766.rs" 11 8 11 16] F0.f _2);

creusot/tests/should_succeed/closures/01_basic.mlcfg

@@ -508,7 +508,7 @@ module C01Basic_MoveMut_Closure0
     goto BB1
   }
   BB1 {
-    _2 <- Borrow.borrow_mut ( * _3);
+    _2 <- Borrow.borrow_final ( * _3) (Borrow.get_id _3);
     _3 <- { _3 with current = ( ^ _2) ; };
     _1 <- { _1 with current = (let C01Basic_MoveMut_Closure0 a =  * _1 in C01Basic_MoveMut_Closure0 _2) ; };
     _2 <- any borrowed uint32;

creusot/tests/should_succeed/closures/05_map.mlcfg

@@ -962,7 +962,7 @@ module C05Map_Impl0_Next
     goto BB0
   }
   BB0 {
-    _3 <- Borrow.borrow_mut (C05Map_Map_Type.map_iter ( * self));
+    _3 <- Borrow.borrow_final (C05Map_Map_Type.map_iter ( * self)) (Borrow.inherit_id (Borrow.get_id self) 1);
     self <- { self with current = (let C05Map_Map_Type.C_Map a b =  * self in C05Map_Map_Type.C_Map ( ^ _3) b) ; };
     assume { Inv0.inv ( ^ _3) };
     _2 <- ([#"../05_map.rs" 18 14 18 30] Next0.next _3);

creusot/tests/should_succeed/drop_pair.mlcfg

@@ -163,7 +163,7 @@ module DropPair_Drop
   }
   BB0 {
     assume { Resolve0.resolve _x };
-    _3 <- Borrow.borrow_mut ( * y);
+    _3 <- Borrow.borrow_final ( * y) (Borrow.get_id y);
     y <- { y with current = ( ^ _3) ; };
     _x <- _3;
     _3 <- any borrowed uint32;

creusot/tests/should_succeed/hashmap.mlcfg

@@ -1782,18 +1782,18 @@ module Hashmap_Impl5_Add
     index <- ([#"../hashmap.rs" 110 27 110 55] UIntSize.of_int (UInt64.to_int _13) % _15);
     _13 <- any uint64;
     _15 <- any usize;
-    _20 <- Borrow.borrow_mut (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self));
+    _20 <- Borrow.borrow_final (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self)) (Borrow.inherit_id (Borrow.get_id self) 1);
     self <- { self with current = (let Hashmap_MyHashMap_Type.C_MyHashMap a =  * self in Hashmap_MyHashMap_Type.C_MyHashMap ( ^ _20)) ; };
     assume { Inv1.inv ( ^ _20) };
     _19 <- ([#"../hashmap.rs" 111 39 111 58] IndexMut0.index_mut _20 index);
     _20 <- any borrowed (Alloc_Vec_Vec_Type.t_vec (Hashmap_List_Type.t_list (k, v)) (Alloc_Alloc_Global_Type.t_global));
     goto BB5
   }
   BB5 {
-    _18 <- Borrow.borrow_mut ( * _19);
+    _18 <- Borrow.borrow_final ( * _19) (Borrow.get_id _19);
     _19 <- { _19 with current = ( ^ _18) ; };
     assume { Inv2.inv ( ^ _18) };
-    l <- Borrow.borrow_mut ( * _18);
+    l <- Borrow.borrow_final ( * _18) (Borrow.get_id _18);
     _18 <- { _18 with current = ( ^ l) ; };
     assume { Inv2.inv ( ^ l) };
     assert { [@expl:type invariant] Inv3.inv _18 };
@@ -1825,13 +1825,13 @@ module Hashmap_Impl5_Add
     goto BB10
   }
   BB10 {
-    k <- Borrow.borrow_mut (let (a, _) = Hashmap_List_Type.cons_0 ( * l) in a);
+    k <- Borrow.borrow_final (let (a, _) = Hashmap_List_Type.cons_0 ( * l) in a) (Borrow.inherit_id (Borrow.inherit_id (Borrow.get_id l) 1) 1);
     l <- { l with current = (let Hashmap_List_Type.C_Cons a b =  * l in Hashmap_List_Type.C_Cons (let (a, b) = Hashmap_List_Type.cons_0 ( * l) in ( ^ k, b)) b) ; };
     assume { Inv6.inv ( ^ k) };
-    v <- Borrow.borrow_mut (let (_, a) = Hashmap_List_Type.cons_0 ( * l) in a);
+    v <- Borrow.borrow_final (let (_, a) = Hashmap_List_Type.cons_0 ( * l) in a) (Borrow.inherit_id (Borrow.inherit_id (Borrow.get_id l) 1) 2);
     l <- { l with current = (let Hashmap_List_Type.C_Cons a b =  * l in Hashmap_List_Type.C_Cons (let (a, b) = Hashmap_List_Type.cons_0 ( * l) in (a,  ^ v)) b) ; };
     assume { Inv7.inv ( ^ v) };
-    tl <- Borrow.borrow_mut (Hashmap_List_Type.cons_1 ( * l));
+    tl <- Borrow.borrow_final (Hashmap_List_Type.cons_1 ( * l)) (Borrow.inherit_id (Borrow.get_id l) 2);
     l <- { l with current = (let Hashmap_List_Type.C_Cons a b =  * l in Hashmap_List_Type.C_Cons a ( ^ tl)) ; };
     assume { Inv8.inv ( ^ tl) };
     tl1 <- tl;
@@ -1875,7 +1875,7 @@ module Hashmap_Impl5_Add
     _46 <- Borrow.borrow_mut ( * tl1);
     tl1 <- { tl1 with current = ( ^ _46) ; };
     assume { Inv2.inv ( ^ _46) };
-    _45 <- Borrow.borrow_mut ( * _46);
+    _45 <- Borrow.borrow_final ( * _46) (Borrow.get_id _46);
     _46 <- { _46 with current = ( ^ _45) ; };
     assume { Inv2.inv ( ^ _45) };
     assert { [@expl:type invariant] Inv3.inv l };
@@ -2785,7 +2785,7 @@ module Hashmap_Impl5_Resize
     _28 <- Borrow.borrow_mut ( * _29);
     _29 <- { _29 with current = ( ^ _28) ; };
     assume { Inv5.inv ( ^ _28) };
-    _27 <- Borrow.borrow_mut ( * _28);
+    _27 <- Borrow.borrow_final ( * _28) (Borrow.get_id _28);
     _28 <- { _28 with current = ( ^ _27) ; };
     assume { Inv5.inv ( ^ _27) };
     l <- ([#"../hashmap.rs" 177 33 177 83] Replace0.replace _27 (Hashmap_List_Type.C_Nil));