diff options
author | qadeer <qadeer@microsoft.com> | 2015-04-18 17:46:27 -0700 |
---|---|---|
committer | qadeer <qadeer@microsoft.com> | 2015-04-18 17:46:27 -0700 |
commit | 6d56652342dd935f47ce5396d7f7d3a480bbb68e (patch) | |
tree | 2dfaf12a8f06dd5a8be3030567bb6413e4ca041b /Test | |
parent | 7c950ff9a2444a4664243be1eb9fe744d1f4fc87 (diff) |
patched ghost checking
Diffstat (limited to 'Test')
-rw-r--r-- | Test/og/ghost.bpl | 27 | ||||
-rw-r--r-- | Test/og/ghost.bpl.expect | 2 |
2 files changed, 29 insertions, 0 deletions
diff --git a/Test/og/ghost.bpl b/Test/og/ghost.bpl new file mode 100644 index 00000000..ef40a232 --- /dev/null +++ b/Test/og/ghost.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure ghost(y: int) returns (z: int) +requires y == 1; +ensures z == 2; +{ + z := y + 1; +} + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:ghost} a: int; + var {:ghost} b: int; + + yield; + call a := ghost(1); + assert {:layer 1} a == 2; + par Incr() | Incr(); + yield; +} + diff --git a/Test/og/ghost.bpl.expect b/Test/og/ghost.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/og/ghost.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors |