diff options
Diffstat (limited to 'Chalice/tests/general-tests/prog4.chalice')
| -rw-r--r-- | Chalice/tests/general-tests/prog4.chalice | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/Chalice/tests/general-tests/prog4.chalice b/Chalice/tests/general-tests/prog4.chalice deleted file mode 100644 index 3c655c71..00000000 --- a/Chalice/tests/general-tests/prog4.chalice +++ /dev/null @@ -1,53 +0,0 @@ -class LoopTargets {
- method M() returns (y) {
- y := 0
- while (y < 100) { y := y + 1 }
- assert y == 0 // error (139)
- }
- method N() returns (t: LoopTargets)
- lockchange t
- {
- t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- lockchange t
- {
- release t // error: loop invariant does not say holds(t) (252)
- s := false
- }
- }
- method P() {
- var t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- invariant acc(t.mu) && waitlevel == t.mu
- lockchange t
- {
- release t // error: loop invariant does not say holds(t) (414)
- acquire t
- s := false
- }
- release t
- }
- method Q() {
- var t := new LoopTargets
- share t
- acquire t
- var s := true
- while (s)
- invariant rd(t.mu)
- invariant holds(t) && waitlevel == t.mu
- lockchange t
- {
- release t
- acquire t
- s := false
- }
- assert holds(t) // there we are
- release t
- }
-}
|