bug fix in the type checking of calls to atomic procedures

3 files changed, 24 insertions, 7 deletions

diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl
new file mode 100644
index 00000000..070cfec4
--- /dev/null
+++ b/Test/civl/chris8.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} x:int;
+
+procedure{:layer 1}{:extern} P1(i:int);
+procedure{:pure}{:extern} P2(j:int);
+
+procedure{:yields}{:layer 1,2} A1({:layer 1}i:int)
+  ensures {:atomic} |{ A: return true; }|;
+{
+  yield;
+  call P1(i);
+  call P2(i);
+  yield;
+}
diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris8.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 39dad919..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
 ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
 {
    var t: int;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
-   var {:ghost} {:layer 3} oldStatusT:bool;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
+   var {:layer 3} oldStatusT:bool;
    
    call oldH, oldT := GhostRead();
    yield;
@@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;
@@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;