diff options
| author |  jansmans <unknown> | 2009-10-02 15:00:11 +0000 |
|---|---|---|
| committer | jansmans <unknown> | 2009-10-02 15:00:11 +0000 |
| commit | bdaa9996170aed0b2638962014fe80777b98d5c7 (patch) | |
| tree | 4f317bacabe5d937a92a07410c952e82716b47f6 /Chalice/src/Boogie.scala | |
| parent | b63ea1d301407ea0b7e1c7d23a243a9c9cc836b9 (diff) | |
- where clauses are now properly type-checked
- all credits must be consumed on entry to a loop by the invariant (to avoid getting the wrong maxlock)
Diffstat (limited to 'Chalice/src/Boogie.scala')
0 files changed, 0 insertions, 0 deletions