diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-05 22:11:09 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-05 22:11:09 -0700 |
| commit | 3feed5acae37f5cfcbb6b25d25117d70faa3e430 (patch) | |
| tree | a2002813e9d362a085d1f57ab061f754b66490f6 /Test/dafny0/TypeTests.dfy | |
| parent | bbfefea4f221c0be1b295ba1c5ee622fda9ec0d0 (diff) | |
improved and fixed compilation and resolution of assign-such-that statements
Diffstat (limited to 'Test/dafny0/TypeTests.dfy')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 2dea7a52..42457918 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -101,10 +101,8 @@ method M() ghost var k: int, l: int;
var m: int;
- // These three statements are allowed by the resolver, but the compiler will complain
- // if it ever gets them.
k :| k < 10;
- k, m :| 0 <= k < m;
+ k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
m :| m < 10;
// Because of the ghost guard, these 'if' statements are ghost contexts, so only
|