Undo civl test changes

boogie-org · Oct 6, 2024 · 6bff2ff · 6bff2ff
1 parent 8ea0f08
commit 6bff2ff
Show file tree

Hide file tree

Showing 14 changed files with 25 additions and 4 deletions.
diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
+    public static readonly IToken /*!*/ ReportedNoToken = new Token();
+
     public static Block Block(string label, List<Cmd> cmds)
     {
-      return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
+      return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
     }
 
     public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
     {
-      return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
+      return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
     }
   }
 

diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs
@@ -33,8 +33,7 @@ public string /*!*/
 
     public Token next; // ML 2005-03-11 Tokens are kept in linked list
 
-    public static readonly IToken /*!*/
-      NoToken = new Token();
+    public static readonly IToken /*!*/ NoToken = new Token();
 
     public Token()
     {

diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
@@ -1,4 +1,5 @@
 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,5 +10,6 @@ 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,5 +2,6 @@ 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,8 +2,10 @@ 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,5 +1,6 @@
 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,5 +2,6 @@ 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,5 +7,6 @@ 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,6 +5,7 @@ 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,5 +1,6 @@
 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,21 +5,25 @@ 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
@@ -28,5 +32,6 @@ 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,11 +1,15 @@
 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,5 +2,6 @@ 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