Civl test refactoring (#754)

boogie-org · Jun 20, 2023 · 980ca54 · 980ca54
1 parent 1969ad0
commit 980ca54
Show file tree

Hide file tree

Showing 76 changed files with 4 additions and 4 deletions.
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
@@ -3505,12 +3505,12 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
         {
           if (callerActionDecl.Creates.All(x => x.ActionName != datatypeTypeCtorDecl.Name))
           {
-            tc.Error(this, "primitive instantiated on type not in the creates clause of caller");
+            tc.Error(this, "primitive call must be instantiated with a pending async type in the creates clause of caller");
           }
         }
         else
         {
-          tc.Error(this, "type parameter to primitive call must be instantiated with a pending async type");
+          tc.Error(this, "primitive call must be instantiated with a pending async type");
         }
       }
       else if (Proc is ActionDecl calleeActionDecl)
@@ -3534,7 +3534,7 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
       }
       else
       {
-        tc.Error(this, "an action may only call actions or pending async primitives");
+        tc.Error(this, "an action may only call actions or primitives");
       }
     }
 

diff --git a/Test/civl/regression-tests/pending-async-2.bpl.expect b/Test/civl/regression-tests/pending-async-2.bpl.expect
@@ -1,2 +1,2 @@
-pending-async-2.bpl(17,2): Error: primitive instantiated on type not in the creates clause of caller
+pending-async-2.bpl(17,2): Error: primitive call must be instantiated with a pending async type in the creates clause of caller
 1 type checking errors detected in pending-async-2.bpl
diff --git a/Test/civl/DeviceCache.bpl → Test/civl/samples/DeviceCache.bpl b/Test/civl/DeviceCache.bpl → Test/civl/samples/DeviceCache.bpl
diff --git a/Test/civl/DeviceCache.bpl.expect → Test/civl/samples/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect → Test/civl/samples/DeviceCache.bpl.expect
diff --git a/Test/civl/FlanaganQadeer.bpl → Test/civl/samples/FlanaganQadeer.bpl b/Test/civl/FlanaganQadeer.bpl → Test/civl/samples/FlanaganQadeer.bpl
diff --git a/Test/civl/FlanaganQadeer.bpl.expect → Test/civl/samples/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect → Test/civl/samples/FlanaganQadeer.bpl.expect
diff --git a/Test/civl/GC.bpl → Test/civl/samples/GC.bpl b/Test/civl/GC.bpl → Test/civl/samples/GC.bpl
diff --git a/Test/civl/GC.bpl.expect → Test/civl/samples/GC.bpl.expect b/Test/civl/GC.bpl.expect → Test/civl/samples/GC.bpl.expect
diff --git a/Test/civl/Program2.bpl → Test/civl/samples/Program2.bpl b/Test/civl/Program2.bpl → Test/civl/samples/Program2.bpl
diff --git a/Test/civl/Program2.bpl.expect → Test/civl/samples/Program2.bpl.expect b/Test/civl/Program2.bpl.expect → Test/civl/samples/Program2.bpl.expect
diff --git a/Test/civl/Program3.bpl → Test/civl/samples/Program3.bpl b/Test/civl/Program3.bpl → Test/civl/samples/Program3.bpl
diff --git a/Test/civl/Program3.bpl.expect → Test/civl/samples/Program3.bpl.expect b/Test/civl/Program3.bpl.expect → Test/civl/samples/Program3.bpl.expect
diff --git a/Test/civl/Program4-fail.bpl → Test/civl/samples/Program4-fail.bpl b/Test/civl/Program4-fail.bpl → Test/civl/samples/Program4-fail.bpl
diff --git a/Test/civl/Program4-fail.bpl.expect → Test/civl/samples/Program4-fail.bpl.expect b/Test/civl/Program4-fail.bpl.expect → Test/civl/samples/Program4-fail.bpl.expect
diff --git a/Test/civl/Program4.bpl → Test/civl/samples/Program4.bpl b/Test/civl/Program4.bpl → Test/civl/samples/Program4.bpl
diff --git a/Test/civl/Program4.bpl.expect → Test/civl/samples/Program4.bpl.expect b/Test/civl/Program4.bpl.expect → Test/civl/samples/Program4.bpl.expect
diff --git a/Test/civl/Siddharth-queue.bpl → Test/civl/samples/Siddharth-queue.bpl b/Test/civl/Siddharth-queue.bpl → Test/civl/samples/Siddharth-queue.bpl
diff --git a/Test/civl/Siddharth-queue.bpl.expect → Test/civl/samples/Siddharth-queue.bpl.expect b/Test/civl/Siddharth-queue.bpl.expect → Test/civl/samples/Siddharth-queue.bpl.expect
diff --git a/Test/civl/StoreBuffer.bpl → Test/civl/samples/StoreBuffer.bpl b/Test/civl/StoreBuffer.bpl → Test/civl/samples/StoreBuffer.bpl
diff --git a/Test/civl/StoreBuffer.bpl.expect → Test/civl/samples/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect → Test/civl/samples/StoreBuffer.bpl.expect
diff --git a/Test/civl/alloc-mem.bpl → Test/civl/samples/alloc-mem.bpl b/Test/civl/alloc-mem.bpl → Test/civl/samples/alloc-mem.bpl
diff --git a/Test/civl/alloc-mem.bpl.expect → Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/alloc-mem.bpl.expect → Test/civl/samples/alloc-mem.bpl.expect
diff --git a/Test/civl/alloc-tid.bpl → Test/civl/samples/alloc-tid.bpl b/Test/civl/alloc-tid.bpl → Test/civl/samples/alloc-tid.bpl
diff --git a/Test/civl/alloc-tid.bpl.expect → Test/civl/samples/alloc-tid.bpl.expect b/Test/civl/alloc-tid.bpl.expect → Test/civl/samples/alloc-tid.bpl.expect
diff --git a/Test/civl/array-insert.bpl → Test/civl/samples/array-insert.bpl b/Test/civl/array-insert.bpl → Test/civl/samples/array-insert.bpl
diff --git a/Test/civl/array-insert.bpl.expect → Test/civl/samples/array-insert.bpl.expect b/Test/civl/array-insert.bpl.expect → Test/civl/samples/array-insert.bpl.expect
diff --git a/Test/civl/bluetooth.bpl → Test/civl/samples/bluetooth.bpl b/Test/civl/bluetooth.bpl → Test/civl/samples/bluetooth.bpl
diff --git a/Test/civl/bluetooth.bpl.expect → Test/civl/samples/bluetooth.bpl.expect b/Test/civl/bluetooth.bpl.expect → Test/civl/samples/bluetooth.bpl.expect
diff --git a/Test/civl/cav2020-1.bpl → Test/civl/samples/cav2020-1.bpl b/Test/civl/cav2020-1.bpl → Test/civl/samples/cav2020-1.bpl
diff --git a/Test/civl/cav2020-1.bpl.expect → Test/civl/samples/cav2020-1.bpl.expect b/Test/civl/cav2020-1.bpl.expect → Test/civl/samples/cav2020-1.bpl.expect
diff --git a/Test/civl/cav2020-2.bpl → Test/civl/samples/cav2020-2.bpl b/Test/civl/cav2020-2.bpl → Test/civl/samples/cav2020-2.bpl
diff --git a/Test/civl/cav2020-2.bpl.expect → Test/civl/samples/cav2020-2.bpl.expect b/Test/civl/cav2020-2.bpl.expect → Test/civl/samples/cav2020-2.bpl.expect
diff --git a/Test/civl/cav2020-3.bpl → Test/civl/samples/cav2020-3.bpl b/Test/civl/cav2020-3.bpl → Test/civl/samples/cav2020-3.bpl
diff --git a/Test/civl/cav2020-3.bpl.expect → Test/civl/samples/cav2020-3.bpl.expect b/Test/civl/cav2020-3.bpl.expect → Test/civl/samples/cav2020-3.bpl.expect
diff --git a/Test/civl/cav2020-talk.bpl → Test/civl/samples/cav2020-talk.bpl b/Test/civl/cav2020-talk.bpl → Test/civl/samples/cav2020-talk.bpl
diff --git a/Test/civl/cav2020-talk.bpl.expect → Test/civl/samples/cav2020-talk.bpl.expect b/Test/civl/cav2020-talk.bpl.expect → Test/civl/samples/cav2020-talk.bpl.expect
diff --git a/Test/civl/civl-paper.bpl → Test/civl/samples/civl-paper.bpl b/Test/civl/civl-paper.bpl → Test/civl/samples/civl-paper.bpl
diff --git a/Test/civl/civl-paper.bpl.expect → Test/civl/samples/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect → Test/civl/samples/civl-paper.bpl.expect
diff --git a/Test/civl/freund.bpl → Test/civl/samples/freund.bpl b/Test/civl/freund.bpl → Test/civl/samples/freund.bpl
diff --git a/Test/civl/freund.bpl.expect → Test/civl/samples/freund.bpl.expect b/Test/civl/freund.bpl.expect → Test/civl/samples/freund.bpl.expect
diff --git a/Test/civl/lamport.bpl → Test/civl/samples/lamport.bpl b/Test/civl/lamport.bpl → Test/civl/samples/lamport.bpl
diff --git a/Test/civl/lamport.bpl.expect → Test/civl/samples/lamport.bpl.expect b/Test/civl/lamport.bpl.expect → Test/civl/samples/lamport.bpl.expect
diff --git a/Test/civl/lease.bpl → Test/civl/samples/lease.bpl b/Test/civl/lease.bpl → Test/civl/samples/lease.bpl
diff --git a/Test/civl/lease.bpl.expect → Test/civl/samples/lease.bpl.expect b/Test/civl/lease.bpl.expect → Test/civl/samples/lease.bpl.expect
diff --git a/Test/civl/lipton.bpl → Test/civl/samples/lipton.bpl b/Test/civl/lipton.bpl → Test/civl/samples/lipton.bpl
diff --git a/Test/civl/lipton.bpl.expect → Test/civl/samples/lipton.bpl.expect b/Test/civl/lipton.bpl.expect → Test/civl/samples/lipton.bpl.expect
diff --git a/Test/civl/lock-introduced.bpl → Test/civl/samples/lock-introduced.bpl b/Test/civl/lock-introduced.bpl → Test/civl/samples/lock-introduced.bpl
diff --git a/Test/civl/lock-introduced.bpl.expect → Test/civl/samples/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect → Test/civl/samples/lock-introduced.bpl.expect
diff --git a/Test/civl/multiset.bpl → Test/civl/samples/multiset.bpl b/Test/civl/multiset.bpl → Test/civl/samples/multiset.bpl
diff --git a/Test/civl/multiset.bpl.expect → Test/civl/samples/multiset.bpl.expect b/Test/civl/multiset.bpl.expect → Test/civl/samples/multiset.bpl.expect
diff --git a/Test/civl/ogcounter.bpl → Test/civl/samples/ogcounter.bpl b/Test/civl/ogcounter.bpl → Test/civl/samples/ogcounter.bpl
diff --git a/Test/civl/ogcounter.bpl.expect → Test/civl/samples/ogcounter.bpl.expect b/Test/civl/ogcounter.bpl.expect → Test/civl/samples/ogcounter.bpl.expect
diff --git a/Test/civl/ogcounter2.bpl → Test/civl/samples/ogcounter2.bpl b/Test/civl/ogcounter2.bpl → Test/civl/samples/ogcounter2.bpl
diff --git a/Test/civl/ogcounter2.bpl.expect → Test/civl/samples/ogcounter2.bpl.expect b/Test/civl/ogcounter2.bpl.expect → Test/civl/samples/ogcounter2.bpl.expect
diff --git a/Test/civl/par-incr.bpl → Test/civl/samples/par-incr.bpl b/Test/civl/par-incr.bpl → Test/civl/samples/par-incr.bpl
diff --git a/Test/civl/par-incr.bpl.expect → Test/civl/samples/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect → Test/civl/samples/par-incr.bpl.expect
diff --git a/Test/civl/purity-issta.bpl → Test/civl/samples/purity-issta.bpl b/Test/civl/purity-issta.bpl → Test/civl/samples/purity-issta.bpl
diff --git a/Test/civl/purity-issta.bpl.expect → Test/civl/samples/purity-issta.bpl.expect b/Test/civl/purity-issta.bpl.expect → Test/civl/samples/purity-issta.bpl.expect
diff --git a/Test/civl/reserve.bpl → Test/civl/samples/reserve.bpl b/Test/civl/reserve.bpl → Test/civl/samples/reserve.bpl
diff --git a/Test/civl/reserve.bpl.expect → Test/civl/samples/reserve.bpl.expect b/Test/civl/reserve.bpl.expect → Test/civl/samples/reserve.bpl.expect
diff --git a/Test/civl/rwlock.bpl → Test/civl/samples/rwlock.bpl b/Test/civl/rwlock.bpl → Test/civl/samples/rwlock.bpl
diff --git a/Test/civl/rwlock.bpl.expect → Test/civl/samples/rwlock.bpl.expect b/Test/civl/rwlock.bpl.expect → Test/civl/samples/rwlock.bpl.expect
diff --git a/Test/civl/seqlock.bpl → Test/civl/samples/seqlock.bpl b/Test/civl/seqlock.bpl → Test/civl/samples/seqlock.bpl
diff --git a/Test/civl/seqlock.bpl.expect → Test/civl/samples/seqlock.bpl.expect b/Test/civl/seqlock.bpl.expect → Test/civl/samples/seqlock.bpl.expect
diff --git a/Test/civl/ticket.bpl → Test/civl/samples/ticket.bpl b/Test/civl/ticket.bpl → Test/civl/samples/ticket.bpl
diff --git a/Test/civl/ticket.bpl.expect → Test/civl/samples/ticket.bpl.expect b/Test/civl/ticket.bpl.expect → Test/civl/samples/ticket.bpl.expect
diff --git a/Test/civl/treiber-stack.bpl → Test/civl/samples/treiber-stack.bpl b/Test/civl/treiber-stack.bpl → Test/civl/samples/treiber-stack.bpl
diff --git a/Test/civl/treiber-stack.bpl.expect → Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect → Test/civl/samples/treiber-stack.bpl.expect
diff --git a/Test/civl/verified-ft.bpl → Test/civl/samples/verified-ft.bpl b/Test/civl/verified-ft.bpl → Test/civl/samples/verified-ft.bpl
diff --git a/Test/civl/verified-ft.bpl.expect → Test/civl/samples/verified-ft.bpl.expect b/Test/civl/verified-ft.bpl.expect → Test/civl/samples/verified-ft.bpl.expect
diff --git a/Test/civl/wilcox.bpl → Test/civl/samples/wilcox.bpl b/Test/civl/wilcox.bpl → Test/civl/samples/wilcox.bpl
diff --git a/Test/civl/wilcox.bpl.expect → Test/civl/samples/wilcox.bpl.expect b/Test/civl/wilcox.bpl.expect → Test/civl/samples/wilcox.bpl.expect
diff --git a/Test/civl/write-barrier.bpl → Test/civl/samples/write-barrier.bpl b/Test/civl/write-barrier.bpl → Test/civl/samples/write-barrier.bpl
diff --git a/Test/civl/write-barrier.bpl.expect → Test/civl/samples/write-barrier.bpl.expect b/Test/civl/write-barrier.bpl.expect → Test/civl/samples/write-barrier.bpl.expect
diff --git a/Test/civl/zeldovich.bpl → Test/civl/samples/zeldovich.bpl b/Test/civl/zeldovich.bpl → Test/civl/samples/zeldovich.bpl
diff --git a/Test/civl/zeldovich.bpl.expect → Test/civl/samples/zeldovich.bpl.expect b/Test/civl/zeldovich.bpl.expect → Test/civl/samples/zeldovich.bpl.expect