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 | c52a162200ed964b332433055d145ec9cb2eadc7 (patch) | |
| tree | af5eec53544205865bf2ae65ffb2617500f959ef /Test/dafny0/ResolutionErrors.dfy | |
| parent | fb76504a943c1fa76c7aceec9dc81de4c35f08c8 (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 {
|