diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-08-03 05:05:45 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-08-03 05:05:45 -0700 |
| commit | d84a7067189e9f11448a97ff406d538e03e4a2e0 (patch) | |
| tree | 6a3dbf635bd263cf1e3bc300c1f5ae0153eaed69 /Test/dafny0/ResolutionErrors.dfy | |
| parent | c340edca6f8675c651eb01515489f61f01c2b0b7 (diff) | |
Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative)
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f8adaad5..1b68ad91 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -24,6 +24,15 @@ method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int) var z := b[m, n, m, n]; // error
}
+method SB(b: array2<int>, s: int) returns (x: int, y: int)
+ requires b != null;
+{
+ while
+ {
+ case b[x,y] == s =>
+ }
+}
+
// -------- name resolution
class Global {
|