diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
| commit | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch) | |
| tree | 8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Test/civl/ghost.bpl | |
| parent | 64e8b33656140b87137d0662d9e6835e004d13c2 (diff) | |
| parent | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff) | |
Merge branch 'upstream' into dfsg_free
Diffstat (limited to 'Test/civl/ghost.bpl')
| -rw-r--r-- | Test/civl/ghost.bpl | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl index 74d16acf..1468fa56 100644 --- a/Test/civl/ghost.bpl +++ b/Test/civl/ghost.bpl @@ -5,7 +5,7 @@ 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) +procedure {:pure} ghost(y: int) returns (z: int) requires y == 1; ensures z == 2; { @@ -15,8 +15,7 @@ ensures z == 2; procedure {:yields} {:layer 1,2} Incr2() ensures {:right} |{ A: x := x + 2; return true; }|; { - var {:ghost} a: int; - var {:ghost} b: int; + var {:layer 1} a: int; yield; call a := ghost(1); @@ -25,7 +24,7 @@ ensures {:right} |{ A: x := x + 2; return true; }|; yield; } -procedure ghost_0() returns (z: int) +procedure {:layer 1} ghost_0() returns (z: int) ensures z == x; { z := x; @@ -34,8 +33,8 @@ ensures z == x; procedure {:yields} {:layer 1,2} Incr2_0() ensures {:right} |{ A: x := x + 2; return true; }|; { - var {:ghost} a: int; - var {:ghost} b: int; + var {:layer 1} a: int; + var {:layer 1} b: int; yield; call a := ghost_0(); |