diff options
| author |  Shaz Qadeer <qadeer@microsoft.com> | 2015-09-25 12:05:19 -0700 |
|---|---|---|
| committer | Shaz Qadeer <qadeer@microsoft.com> | 2015-09-25 12:05:19 -0700 |
| commit | 5927744da636063556118f469cc8f9354b1cabe6 (patch) | |
| tree | 94b1395b54dfbe28485f68d211d192bdeef9881a /Test/civl/ghost.bpl | |
| parent | 437bde8d029afab9631e5ce539600dcfcaeace42 (diff) | |
added introduced and ghost local variables
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(); |