diff options
author | Shaz Qadeer <qadeer@microsoft.com> | 2015-10-16 14:08:21 -0700 |
---|---|---|
committer | Shaz Qadeer <qadeer@microsoft.com> | 2015-10-16 14:08:21 -0700 |
commit | a6b78b0ea28c22744fa846d7729b5c50247f9987 (patch) | |
tree | 0d7365c7b4a944221f4aece13cfb061bbe63e57c /Test/civl/chris8.bpl | |
parent | bad6c014fdf57c5674a840b32047c7db54cd7aba (diff) |
bug fix in the type checking of calls to atomic procedures
Diffstat (limited to 'Test/civl/chris8.bpl')
-rw-r--r-- | Test/civl/chris8.bpl | 15 |
1 files changed, 15 insertions, 0 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; +} |