add mover types

boogie-org · Jun 27, 2024 · a3c6a22 · a3c6a22
1 parent 1443489
commit a3c6a22
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl b/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl
@@ -36,7 +36,7 @@ creates read_f;
     call create_asyncs((lambda pa:read_f :: 1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid));
 }
 
-action {:layer 2} main_f'(tid: Tid, {:linear_in} sps: Set Permission)
+async action {:layer 2} main_f'(tid: Tid, {:linear_in} sps: Set Permission)
 modifies pSet, channels;
 {
     var snapshot: [int]StampedValue;  
@@ -116,7 +116,7 @@ modifies channels;
     channels[tid] := Some(snapshot);
 }
 
-action {:layer 1,2} ChannelReceive(tid: Tid) returns (snapshot: [int]StampedValue)
+right action {:layer 1,2} ChannelReceive(tid: Tid) returns (snapshot: [int]StampedValue)
 modifies channels;
 {
     assume channels[tid] != None();
@@ -135,7 +135,7 @@ creates read_s;
     call create_asyncs((lambda pa:read_s :: 1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid));
 }
 
-action {:layer 2} main_s'(tid: Tid, {:linear_in} sps: Set Permission)
+async action {:layer 2} main_s'(tid: Tid, {:linear_in} sps: Set Permission)
 modifies pSet, channels;
 {
     var snapshot: [int]StampedValue;  

diff --git a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect b/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 45 verified, 0 errors
+Boogie program verifier finished with 57 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,2 @@

		Boogie program verifier finished with 45 verified, 0 errors
		Boogie program verifier finished with 57 verified, 0 errors