Update spans

creusot-rs · Mar 11, 2024 · 60b7c2d · 60b7c2d
1 parent 6276214
commit 60b7c2d
Show file tree

Hide file tree

Showing 193 changed files with 2,234 additions and 2,306 deletions.
diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg b/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg
@@ -131,15 +131,15 @@ module C01ResolveUnsoundness_MakeVecOfSize
     goto BB1
   }
   BB1 {
-    [#"../01_resolve_unsoundness.rs" 11 16 11 17] i <- ([#"../01_resolve_unsoundness.rs" 11 16 11 17] (0 : usize));
+    [#"../01_resolve_unsoundness.rs" 11 16 11 17] i <- (0 : usize);
     goto BB2
   }
   BB2 {
     invariant { [#"../01_resolve_unsoundness.rs" 12 16 12 37] (0 : usize) <= i /\ i <= n };
     goto BB3
   }
   BB3 {
-    [#"../01_resolve_unsoundness.rs" 13 10 13 16] _9 <- ([#"../01_resolve_unsoundness.rs" 13 10 13 16] i <= n);
+    [#"../01_resolve_unsoundness.rs" 13 10 13 16] _9 <- i <= n;
     switch (_9)
       | False -> goto BB6
       | True -> goto BB4
@@ -153,11 +153,11 @@ module C01ResolveUnsoundness_MakeVecOfSize
     goto BB5
   }
   BB5 {
-    [#"../01_resolve_unsoundness.rs" 15 8 15 14] i <- ([#"../01_resolve_unsoundness.rs" 15 8 15 14] i + (1 : usize));
+    [#"../01_resolve_unsoundness.rs" 15 8 15 14] i <- i + (1 : usize);
     goto BB2
   }
   BB6 {
-    [#"../01_resolve_unsoundness.rs" 17 11 17 14] _0 <- ([#"../01_resolve_unsoundness.rs" 17 11 17 14] out);
+    [#"../01_resolve_unsoundness.rs" 17 11 17 14] _0 <- out;
     out <- any Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global);
     goto BB7
   }

diff --git a/creusot/tests/should_fail/bug/222.mlcfg b/creusot/tests/should_fail/bug/222.mlcfg
@@ -106,7 +106,7 @@ module C222_UsesInvariant
     goto BB2
   }
   BB2 {
-    [#"../222.rs" 40 42 42 1] _0 <- ([#"../222.rs" 40 42 42 1] ());
+    [#"../222.rs" 40 42 42 1] _0 <- ();
     return _0
   }
 

diff --git a/creusot/tests/should_fail/bug/492.mlcfg b/creusot/tests/should_fail/bug/492.mlcfg
@@ -52,7 +52,7 @@ module C492_ReborrowTuple
     [#"../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, (32 : uint32)));
+    [#"../492.rs" 6 4 6 11] _0 <- (_3, (32 : uint32));
     _3 <- any borrowed t;
     assert { [@expl:type invariant] inv1 x };
     assume { resolve0 x };
@@ -119,7 +119,7 @@ module C492_Test
     goto BB0
   }
   BB0 {
-    [#"../492.rs" 11 16 11 17] x <- ([#"../492.rs" 11 16 11 17] (5 : int32));
+    [#"../492.rs" 11 16 11 17] x <- (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_final ( * _6) (Borrow.get_id _6);
@@ -129,14 +129,14 @@ module C492_Test
     goto BB1
   }
   BB1 {
-    [#"../492.rs" 12 9 12 12] res <- ([#"../492.rs" 12 9 12 12] let (a, _) = _4 in a);
+    [#"../492.rs" 12 9 12 12] res <- (let (a, _) = _4 in a);
     _4 <- (let (x0, x1) = _4 in (any borrowed int32, x1));
     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] (10 : int32)) ; };
+    [#"../492.rs" 14 4 14 13] res <- { res with current = (10 : int32) ; };
     assume { resolve1 res };
-    [#"../492.rs" 10 14 15 1] _0 <- ([#"../492.rs" 10 14 15 1] ());
+    [#"../492.rs" 10 14 15 1] _0 <- ();
     return _0
   }
 

diff --git a/creusot/tests/should_fail/bug/692.mlcfg b/creusot/tests/should_fail/bug/692.mlcfg
@@ -157,7 +157,7 @@ module C692_Incorrect
     goto BB1
   }
   BB1 {
-    [#"../692.rs" 8 77 8 79] _0 <- ([#"../692.rs" 8 77 8 79] ());
+    [#"../692.rs" 8 77 8 79] _0 <- ();
     goto BB2
   }
   BB2 {
@@ -219,19 +219,19 @@ module C692_ValidNormal_Closure2
       end
   }
   BB1 {
-    [#"../692.rs" 16 25 16 26] _4 <- ([#"../692.rs" 16 25 16 26] (2 : uint32));
+    [#"../692.rs" 16 25 16 26] _4 <- (2 : uint32);
     goto BB3
   }
   BB2 {
-    [#"../692.rs" 16 36 16 37] _4 <- ([#"../692.rs" 16 36 16 37] (1 : uint32));
+    [#"../692.rs" 16 36 16 37] _4 <- (1 : uint32);
     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 = _4 ; })) ; };
     _4 <- any uint32;
     assume { resolve0 _1 };
-    [#"../692.rs" 16 14 16 39] res <- ([#"../692.rs" 16 14 16 39] ());
-    [#"../692.rs" 15 17 15 64] _0 <- ([#"../692.rs" 15 17 15 64] res);
+    [#"../692.rs" 16 14 16 39] res <- ();
+    [#"../692.rs" 15 17 15 64] _0 <- res;
     return _0
   }
 
@@ -267,8 +267,8 @@ module C692_ValidNormal_Closure1
     goto BB0
   }
   BB0 {
-    [#"../692.rs" 14 7 14 15] res <- ([#"../692.rs" 14 7 14 15] field_00 _1 > (7 : uint32));
-    [#"../692.rs" 13 15 13 47] _0 <- ([#"../692.rs" 13 15 13 47] res);
+    [#"../692.rs" 14 7 14 15] res <- field_00 _1 > (7 : uint32);
+    [#"../692.rs" 13 15 13 47] _0 <- res;
     return _0
   }
 
@@ -341,19 +341,19 @@ module C692_ValidNormal
     goto BB0
   }
   BB0 {
-    [#"../692.rs" 12 16 12 20] r <- ([#"../692.rs" 12 16 12 20] (0 : uint32));
-    [#"../692.rs" 13 15 13 47] cond <- ([#"../692.rs" 13 15 13 47] C692_ValidNormal_Closure1.C692_ValidNormal_Closure1 n);
+    [#"../692.rs" 12 16 12 20] r <- (0 : uint32);
+    [#"../692.rs" 13 15 13 47] cond <- C692_ValidNormal_Closure1.C692_ValidNormal_Closure1 n;
     [#"../692.rs" 15 17 15 64] _7 <- Borrow.borrow_mut r;
     [#"../692.rs" 15 17 15 64] r <-  ^ _7;
-    [#"../692.rs" 15 17 15 64] branch <- ([#"../692.rs" 15 17 15 64] C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 _7);
+    [#"../692.rs" 15 17 15 64] branch <- C692_ValidNormal_Closure2.C692_ValidNormal_Closure2 _7;
     _7 <- any borrowed uint32;
     assume { resolve0 cond };
     [#"../692.rs" 17 4 17 27] _8 <- ([#"../692.rs" 17 4 17 27] incorrect0 cond branch);
     branch <- any C692_ValidNormal_Closure2.c692_validnormal_closure2;
     goto BB1
   }
   BB1 {
-    [#"../692.rs" 18 4 18 5] _0 <- ([#"../692.rs" 18 4 18 5] r);
+    [#"../692.rs" 18 4 18 5] _0 <- r;
     return _0
   }
 

diff --git a/creusot/tests/should_fail/bug/695.mlcfg b/creusot/tests/should_fail/bug/695.mlcfg
@@ -193,7 +193,7 @@ module C695_InversedIf
     goto BB2
   }
   BB2 {
-    [#"../695.rs" 7 8 7 14] _7 <- ([#"../695.rs" 7 8 7 14] ());
+    [#"../695.rs" 7 8 7 14] _7 <- ();
     [#"../695.rs" 7 8 7 14] _5 <- ([#"../695.rs" 7 8 7 14] call0 cond _7);
     _7 <- any ();
     goto BB3
@@ -207,7 +207,7 @@ module C695_InversedIf
   BB4 {
     assert { [@expl:type invariant] inv0 cond };
     assume { resolve0 cond };
-    [#"../695.rs" 10 8 10 21] _11 <- ([#"../695.rs" 10 8 10 21] (false));
+    [#"../695.rs" 10 8 10 21] _11 <- (false);
     [#"../695.rs" 10 8 10 21] _0 <- ([#"../695.rs" 10 8 10 21] call_once0 branch _11);
     branch <- any b;
     _11 <- any bool;
@@ -216,7 +216,7 @@ module C695_InversedIf
   BB5 {
     assert { [@expl:type invariant] inv0 cond };
     assume { resolve0 cond };
-    [#"../695.rs" 8 8 8 20] _9 <- ([#"../695.rs" 8 8 8 20] (true));
+    [#"../695.rs" 8 8 8 20] _9 <- (true);
     [#"../695.rs" 8 8 8 20] _0 <- ([#"../695.rs" 8 8 8 20] call_once0 branch _9);
     branch <- any b;
     _9 <- any bool;
@@ -288,19 +288,19 @@ module C695_Valid_Closure2
       end
   }
   BB1 {
-    [#"../695.rs" 20 25 20 26] _4 <- ([#"../695.rs" 20 25 20 26] (2 : uint32));
+    [#"../695.rs" 20 25 20 26] _4 <- (2 : uint32);
     goto BB3
   }
   BB2 {
-    [#"../695.rs" 20 36 20 37] _4 <- ([#"../695.rs" 20 36 20 37] (1 : uint32));
+    [#"../695.rs" 20 36 20 37] _4 <- (1 : uint32);
     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 = _4 ; })) ; };
     _4 <- any uint32;
     assume { resolve0 _1 };
-    [#"../695.rs" 20 14 20 39] res <- ([#"../695.rs" 20 14 20 39] ());
-    [#"../695.rs" 19 17 19 64] _0 <- ([#"../695.rs" 19 17 19 64] res);
+    [#"../695.rs" 20 14 20 39] res <- ();
+    [#"../695.rs" 19 17 19 64] _0 <- res;
     return _0
   }
 
@@ -336,8 +336,8 @@ module C695_Valid_Closure1
     goto BB0
   }
   BB0 {
-    [#"../695.rs" 18 7 18 15] res <- ([#"../695.rs" 18 7 18 15] field_00 _1 > (7 : uint32));
-    [#"../695.rs" 17 15 17 47] _0 <- ([#"../695.rs" 17 15 17 47] res);
+    [#"../695.rs" 18 7 18 15] res <- field_00 _1 > (7 : uint32);
+    [#"../695.rs" 17 15 17 47] _0 <- res;
     return _0
   }
 
@@ -415,11 +415,11 @@ module C695_Valid
     goto BB0
   }
   BB0 {
-    [#"../695.rs" 16 16 16 20] r <- ([#"../695.rs" 16 16 16 20] (0 : uint32));
-    [#"../695.rs" 17 15 17 47] cond <- ([#"../695.rs" 17 15 17 47] C695_Valid_Closure1.C695_Valid_Closure1 n);
+    [#"../695.rs" 16 16 16 20] r <- (0 : uint32);
+    [#"../695.rs" 17 15 17 47] cond <- C695_Valid_Closure1.C695_Valid_Closure1 n;
     [#"../695.rs" 19 17 19 64] _7 <- Borrow.borrow_mut r;
     [#"../695.rs" 19 17 19 64] r <-  ^ _7;
-    [#"../695.rs" 19 17 19 64] branch <- ([#"../695.rs" 19 17 19 64] C695_Valid_Closure2.C695_Valid_Closure2 _7);
+    [#"../695.rs" 19 17 19 64] branch <- C695_Valid_Closure2.C695_Valid_Closure2 _7;
     _7 <- any borrowed uint32;
     assume { resolve0 cond };
     [#"../695.rs" 21 4 21 29] _8 <- ([#"../695.rs" 21 4 21 29] inversed_if0 cond branch);
@@ -428,7 +428,7 @@ module C695_Valid
   }
   BB1 {
     assert { [@expl:assertion] [#"../695.rs" 22 20 22 25] false };
-    [#"../695.rs" 23 4 23 5] _0 <- ([#"../695.rs" 23 4 23 5] r);
+    [#"../695.rs" 23 4 23 5] _0 <- r;
     return _0
   }
 

diff --git a/creusot/tests/should_fail/bug/869.mlcfg b/creusot/tests/should_fail/bug/869.mlcfg
@@ -61,13 +61,13 @@ module C869_Unsound
     goto BB3
   }
   BB3 {
-    [#"../869.rs" 18 4 18 64] evil <- { evil with current = ([#"../869.rs" 18 4 18 64] _15) ; };
+    [#"../869.rs" 18 4 18 64] evil <- { evil with current = _15 ; };
     _15 <- any Snapshot.snap_ty bool;
     assume { resolve0 evil };
     assume { resolve0 xm };
     assert { [@expl:assertion] [#"../869.rs" 19 20 19 37] Snapshot.inner ( * evil) = (not Snapshot.inner ( ^ evil)) };
     assert { [@expl:assertion] [#"../869.rs" 20 20 20 37] Snapshot.inner ( * evil) = (not Snapshot.inner ( * evil)) };
-    [#"../869.rs" 4 17 21 1] _0 <- ([#"../869.rs" 4 17 21 1] ());
+    [#"../869.rs" 4 17 21 1] _0 <- ();
     return _0
   }
 

diff --git a/creusot/tests/should_fail/bug/specialize.mlcfg b/creusot/tests/should_fail/bug/specialize.mlcfg
@@ -62,7 +62,7 @@ module Specialize_F
   }
   BB1 {
     assert { [@expl:assertion] [#"../specialize.rs" 24 20 24 25] false };
-    [#"../specialize.rs" 21 18 25 1] _0 <- ([#"../specialize.rs" 21 18 25 1] ());
+    [#"../specialize.rs" 21 18 25 1] _0 <- ();
     goto BB2
   }
   BB2 {
@@ -126,7 +126,7 @@ module Specialize_G
   }
   BB1 {
     assert { [@expl:assertion] [#"../specialize.rs" 31 20 31 25] false };
-    [#"../specialize.rs" 27 19 32 1] _0 <- ([#"../specialize.rs" 27 19 32 1] ());
+    [#"../specialize.rs" 27 19 32 1] _0 <- ();
     goto BB2
   }
   BB2 {
@@ -191,7 +191,7 @@ module Specialize_H
   }
   BB1 {
     assert { [@expl:assertion] [#"../specialize.rs" 37 20 37 25] false };
-    [#"../specialize.rs" 34 18 38 1] _0 <- ([#"../specialize.rs" 34 18 38 1] ());
+    [#"../specialize.rs" 34 18 38 1] _0 <- ();
     goto BB2
   }
   BB2 {

diff --git a/creusot/tests/should_fail/bug/subregion.mlcfg b/creusot/tests/should_fail/bug/subregion.mlcfg
@@ -15,29 +15,29 @@ module Subregion_ListReversalH
     goto BB0
   }
   BB0 {
-    [#"../subregion.rs" 4 16 4 17] r <- ([#"../subregion.rs" 4 16 4 17] (0 : usize));
+    [#"../subregion.rs" 4 16 4 17] r <- (0 : usize);
     goto BB1
   }
   BB1 {
     invariant { [#"../subregion.rs" 5 16 5 20] true };
     goto BB2
   }
   BB2 {
-    [#"../subregion.rs" 6 10 6 16] _7 <- ([#"../subregion.rs" 6 10 6 16] l <> (0 : usize));
+    [#"../subregion.rs" 6 10 6 16] _7 <- l <> (0 : usize);
     switch (_7)
       | False -> goto BB4
       | True -> goto BB3
       end
   }
   BB3 {
     assert { [@expl:assertion] [#"../subregion.rs" 7 22 7 27] false };
-    [#"../subregion.rs" 8 16 8 17] x <- ([#"../subregion.rs" 8 16 8 17] r);
-    [#"../subregion.rs" 9 18 9 19] tmp <- ([#"../subregion.rs" 9 18 9 19] l);
-    [#"../subregion.rs" 10 8 10 15] r <- ([#"../subregion.rs" 10 8 10 15] tmp);
+    [#"../subregion.rs" 8 16 8 17] x <- r;
+    [#"../subregion.rs" 9 18 9 19] tmp <- l;
+    [#"../subregion.rs" 10 8 10 15] r <- tmp;
     goto BB1
   }
   BB4 {
-    [#"../subregion.rs" 13 11 13 12] _0 <- ([#"../subregion.rs" 13 11 13 12] r);
+    [#"../subregion.rs" 13 11 13 12] _0 <- r;
     return _0
   }
 

diff --git a/creusot/tests/should_fail/final_borrows.mlcfg b/creusot/tests/should_fail/final_borrows.mlcfg
@@ -48,7 +48,7 @@ module FinalBorrows_NotFinalBorrow
     assume { inv0 ( ^ _b2) };
     assert { [@expl:type invariant] inv1 _b2 };
     assume { resolve0 _b2 };
-    [#"../final_borrows.rs" 5 40 9 1] _0 <- ([#"../final_borrows.rs" 5 40 9 1] ());
+    [#"../final_borrows.rs" 5 40 9 1] _0 <- ();
     assert { [@expl:type invariant] inv1 bor };
     assume { resolve0 bor };
     return _0
@@ -106,7 +106,7 @@ module FinalBorrows_StoreChangesProphecy
     goto BB1
   }
   BB1 {
-    [#"../final_borrows.rs" 14 4 14 8] bor <- { bor with current = ([#"../final_borrows.rs" 14 4 14 8] x) ; };
+    [#"../final_borrows.rs" 14 4 14 8] bor <- { bor with current = x ; };
     x <- any t;
     assert { [@expl:type invariant] inv0 ( * bor) };
     assume { resolve1 ( * bor) };
@@ -116,7 +116,7 @@ module FinalBorrows_StoreChangesProphecy
   }
   BB3 {
     assert { [@expl:assertion] [#"../final_borrows.rs" 15 18 15 27] b1 = bor };
-    [#"../final_borrows.rs" 11 52 16 1] _0 <- ([#"../final_borrows.rs" 11 52 16 1] ());
+    [#"../final_borrows.rs" 11 52 16 1] _0 <- ();
     goto BB4
   }
   BB4 {
@@ -134,7 +134,7 @@ module FinalBorrows_CallChangesProphecy_Inner
     goto BB0
   }
   BB0 {
-    [#"../final_borrows.rs" 20 8 20 9] _0 <- ([#"../final_borrows.rs" 20 8 20 9] (2 : int32));
+    [#"../final_borrows.rs" 20 8 20 9] _0 <- (2 : int32);
     return _0
   }
 
@@ -167,11 +167,11 @@ module FinalBorrows_CallChangesProphecy
     goto BB1
   }
   BB1 {
-    [#"../final_borrows.rs" 24 4 24 18] bor <- { bor with current = ([#"../final_borrows.rs" 24 4 24 18] _3) ; };
+    [#"../final_borrows.rs" 24 4 24 18] bor <- { bor with current = _3 ; };
     _3 <- any int32;
     assume { resolve0 bor };
     assert { [@expl:assertion] [#"../final_borrows.rs" 25 18 25 27] b1 = bor };
-    [#"../final_borrows.rs" 18 44 26 1] _0 <- ([#"../final_borrows.rs" 18 44 26 1] ());
+    [#"../final_borrows.rs" 18 44 26 1] _0 <- ();
     return _0
   }
 
@@ -368,9 +368,9 @@ module FinalBorrows_Indexing
     goto BB0
   }
   BB0 {
-    [#"../final_borrows.rs" 38 11 38 12] _6 <- ([#"../final_borrows.rs" 38 11 38 12] (0 : usize));
-    [#"../final_borrows.rs" 38 9 38 13] _7 <- ([#"../final_borrows.rs" 38 9 38 13] Slice.length ( * x));
-    [#"../final_borrows.rs" 38 9 38 13] _8 <- ([#"../final_borrows.rs" 38 9 38 13] _6 < _7);
+    [#"../final_borrows.rs" 38 11 38 12] _6 <- (0 : usize);
+    [#"../final_borrows.rs" 38 9 38 13] _7 <- Slice.length ( * x);
+    [#"../final_borrows.rs" 38 9 38 13] _8 <- _6 < _7;
     assert { [@expl:index in bounds] [#"../final_borrows.rs" 38 9 38 13] _8 };
     goto BB1
   }

diff --git a/creusot/tests/should_fail/opaque_unproveable.mlcfg b/creusot/tests/should_fail/opaque_unproveable.mlcfg
@@ -12,7 +12,7 @@ module OpaqueUnproveable_Test
   }
   BB0 {
     assert { [@expl:assertion] [#"../opaque_unproveable.rs" 16 18 16 29] opaque0 () };
-    [#"../opaque_unproveable.rs" 14 14 17 1] _0 <- ([#"../opaque_unproveable.rs" 14 14 17 1] ());
+    [#"../opaque_unproveable.rs" 14 14 17 1] _0 <- ();
     return _0
   }
 

diff --git a/creusot/tests/should_fail/traits/17_impl_refinement.mlcfg b/creusot/tests/should_fail/traits/17_impl_refinement.mlcfg
@@ -14,7 +14,7 @@ module C17ImplRefinement_Impl0_MyFunction
     goto BB0
   }
   BB0 {
-    [#"../17_impl_refinement.rs" 15 8 15 10] _0 <- ([#"../17_impl_refinement.rs" 15 8 15 10] (20 : usize));
+    [#"../17_impl_refinement.rs" 15 8 15 10] _0 <- (20 : usize);
     return _0
   }