Update test files

boogie-org · Oct 2, 2024 · c1db5a2 · c1db5a2
1 parent d3a9015
commit c1db5a2
Show file tree

Hide file tree

Showing 16 changed files with 29 additions and 50 deletions.
diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
@@ -484,7 +484,7 @@ void ComputeBlockSetsHelper(Block b, bool allowSmall)
         }
       }
 
-      void ComputeBlockSets(bool allowSmall)
+      private void ComputeBlockSets(bool allowSmall)
       {
         protectedFromAssertToAssume.Clear();
         keepAtAll.Clear();
@@ -494,12 +494,12 @@ void ComputeBlockSets(bool allowSmall)
 
         if (assertToAssume)
         {
-          foreach (Block b in allowSmall ? Blocks : bigBlocks)
+          foreach (var block in allowSmall ? Blocks : bigBlocks)
           {
-            Contract.Assert(b != null);
-            if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock)))
+            Contract.Assert(block != null);
+            if (ComputeReachableNodes(block).Contains(cce.NonNull(splitBlock)))
             {
-              keepAtAll.Add(b);
+              keepAtAll.Add(block);
             }
           }
 

diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
@@ -1,5 +1,4 @@
 intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed
 Execution trace:
-    (0,0): init
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect
@@ -10,6 +10,5 @@ Execution trace:
     left-mover.bpl(6,24): inline$inc$0$Return
 left-mover.bpl(26,24): Error: Cooperation check for block failed
 Execution trace:
-    (0,0): init
 
 Boogie program verifier finished with 3 verified, 3 errors
diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect
@@ -2,6 +2,5 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-1.bpl(7,3): anon0
     non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/civl/regression-tests/non-interference-2.bpl.expect b/Test/civl/regression-tests/non-interference-2.bpl.expect
@@ -2,10 +2,8 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(7,3): anon0
     non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(34,3): anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 
 Boogie program verifier finished with 2 verified, 2 errors
diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect
@@ -1,6 +1,5 @@
 pa-noninterference-check.bpl(26,1): Error: Non-interference check failed
 Execution trace:
-    (0,0): init
     pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0
     pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return
 

diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect
@@ -2,6 +2,5 @@ parallel1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     parallel1.bpl(7,3): anon0
     parallel1.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/civl/regression-tests/parallel6.bpl.expect b/Test/civl/regression-tests/parallel6.bpl.expect
@@ -7,6 +7,5 @@ Execution trace:
     parallel6.bpl(11,5): anon0_0
     parallel6.bpl(30,7): inline$atomic_incr$2$anon0
     parallel6.bpl(30,7): inline$atomic_incr$3$anon0
-    (0,0): Civl_ReturnChecker
 
 Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect
@@ -5,7 +5,6 @@ Execution trace:
     pending-async-1.bpl(51,3): anon0$1
     pending-async-1.bpl(11,9): inline$B$1$anon0
     pending-async-1.bpl(51,3): anon0$2
-    (0,0): Civl_ReturnChecker
 pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized
 Execution trace:
     pending-async-1.bpl(67,3): anon0

diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect
@@ -1,6 +1,5 @@
 pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed
 Execution trace:
-    (0,0): init
     pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0
     pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return
 

diff --git a/Test/civl/regression-tests/refinement.bpl.expect b/Test/civl/regression-tests/refinement.bpl.expect
@@ -5,25 +5,21 @@ Execution trace:
     refinement.bpl(10,3): anon0$1
     refinement.bpl(10,3): anon0_0
     refinement.bpl(58,5): inline$INCR$1$anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action
 Execution trace:
     refinement.bpl(18,3): anon0
     refinement.bpl(64,5): inline$DECR$0$anon0
     refinement.bpl(18,3): anon0$1
-    (0,0): Civl_RefinementChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
     refinement.bpl(18,3): anon0
     refinement.bpl(64,5): inline$DECR$0$anon0
     refinement.bpl(18,3): anon0$1
     refinement.bpl(18,3): anon0_0
     refinement.bpl(58,5): inline$INCR$0$anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement.bpl(41,1): anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement.bpl(46,3): anon0
@@ -32,6 +28,5 @@ Execution trace:
     refinement.bpl(46,3): anon0_0
     refinement.bpl(48,3): anon2_LoopHead
     refinement.bpl(58,5): inline$INCR$1$anon0
-    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 3 verified, 5 errors
diff --git a/Test/civl/regression-tests/refinement2.bpl.expect b/Test/civl/regression-tests/refinement2.bpl.expect
@@ -1,15 +1,11 @@
 refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement2.bpl(16,5): anon0
-    (0,0): Civl_call_refinement_4
     refinement2.bpl(27,28): inline$atomic_nop$0$Return
-    (0,0): Civl_ReturnChecker
 refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement2.bpl(16,5): anon0
-    (0,0): Civl_call_refinement_3
     refinement2.bpl(22,7): inline$atomic_incr$0$anon0
     refinement2.bpl(19,28): inline$atomic_incr$0$Return
-    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 1 verified, 2 errors
diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect
@@ -2,6 +2,5 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed
 Execution trace:
     yield-invariant-fails.bpl(11,5): anon0
     yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
@@ -3,18 +3,18 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying Ex ...
-// CHECK:      checking split 1/11 .*
-// CHECK:      checking split 2/11 .*
-// CHECK:      checking split 3/11 .*
-// CHECK:      --> split #3 done,  \[.* s\] Invalid
-// CHECK:      checking split 4/11 .*
-// CHECK:      checking split 5/11 .*
-// CHECK:      checking split 6/11 .*
-// CHECK:      checking split 7/11 .*
-// CHECK:      checking split 8/11 .*
-// CHECK:      checking split 9/11 .*
-// CHECK:      checking split 10/11 .*
-// CHECK:      checking split 11/11 .*
+// CHECK:      checking split 1/12 .*
+// CHECK:      checking split 2/12 .*
+// CHECK:      checking split 3/12 .*
+// CHECK:      checking split 4/12 .*
+// CHECK:      --> split #4 done,  \[.* s\] Invalid
+// CHECK:      checking split 5/12 .*
+// CHECK:      checking split 6/12 .*
+// CHECK:      checking split 7/12 .*
+// CHECK:      checking split 8/12 .*
+// CHECK:      checking split 9/12 .*
+// CHECK:      checking split 10/12 .*
+// CHECK:      checking split 11/12 .*
 // CHECK-L: SplitOnEveryAssert.bpl(31,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)

diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl
@@ -3,18 +3,18 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying DoTheSplitting ...
-// CHECK:      checking split 1/11.*
-// CHECK:      checking split 2/11.*
-// CHECK:      checking split 3/11.*
-// CHECK:      --> split #3 done,  \[.* s\] Invalid
-// CHECK:      checking split 4/11.*
-// CHECK:      checking split 5/11.*
-// CHECK:      checking split 6/11.*
-// CHECK:      checking split 7/11.*
-// CHECK:      checking split 8/11.*
-// CHECK:      checking split 9/11.*
-// CHECK:      checking split 10/11.*
-// CHECK:      checking split 11/11.*
+// CHECK:      checking split 1/12.*
+// CHECK:      checking split 2/12.*
+// CHECK:      checking split 3/12.*
+// CHECK:      checking split 4/12.*
+// CHECK:      --> split #4 done,  \[.* s\] Invalid
+// CHECK:      checking split 5/12.*
+// CHECK:      checking split 6/12.*
+// CHECK:      checking split 7/12.*
+// CHECK:      checking split 8/12.*
+// CHECK:      checking split 9/12.*
+// CHECK:      checking split 10/12.*
+// CHECK:      checking split 11/12.*
 // CHECK-L: SplitOnEveryAssert.bpl(36,5): Error: this assertion could not be proved
 
 // Verify the second procedure is NOT split. .* is necessary to match the blank line in-between.

diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect
@@ -22,6 +22,5 @@ Execution trace:
     Structured.bpl(355,3): anon4_LoopHead
     Structured.bpl(358,7): anon4_LoopBody
     Structured.bpl(361,7): anon5_LoopBody
-    (0,0): anon3
 
 Boogie program verifier finished with 16 verified, 4 errors