From a3c6a220814b266f6e32f89e187bd73d421b29df Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 27 Jun 2024 07:34:26 -0700 Subject: [PATCH] add mover types --- .../inductive-sequentialization/snapshot-scatter-gather.bpl | 6 +++--- .../snapshot-scatter-gather.bpl.expect | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl b/Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl index 5841d9f8a..b07d0ec5d 100644 --- 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 index 6d814241b..753f9e1e3 100644 --- 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 \ No newline at end of file +Boogie program verifier finished with 57 verified, 0 errors \ No newline at end of file