diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-04 18:40:59 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-04 18:40:59 -0700 |
| commit | 659491fddae2ee457100b6fa4c27afef3340621e (patch) | |
| tree | f9538d97ac1e58da751726006d48334d6164ef7d | |
| parent | 3ff2e42970584ad66f8b8e353ddce86dbea92baf (diff) | |
Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 2 | ||||
| -rw-r--r-- | Test/aitest9/TestIntervals.bpl | 16 | ||||
| -rw-r--r-- | Test/aitest9/answer | 2 |
3 files changed, 18 insertions, 2 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 62ebc77f..1367a08d 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1472,7 +1472,7 @@ namespace Microsoft.Boogie { NAryExpr/*!*/ res = Expr.Select(Map.AsExpr, Indexes);
Contract.Assert(res != null);
res.TypeParameters = this.TypeParameters;
- res.Type = Map.AsExpr.Type.AsMap.Result;
+ res.Type = this.Type;
return res;
}
}
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index b989e16c..bee73a57 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -22,3 +22,19 @@ procedure P() assert -3 <= c;
assert c <= 0; // error (there was once an error in the Intervals which thought this assertion to be true)
}
+
+// The following tests a triply nested array, where the innermost array is a polymorphic map.
+// There was once an error in Boogie's handling of such things in the AI code.
+
+type ref;
+type teflon;
+
+type Field a;
+type HeapType = <a>[Field a]a;
+var Heap: HeapType;
+
+procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon)
+ modifies Heap;
+{
+ Heap[myField][r][t] := true;
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer index 27e18ca4..d68508af 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -18,4 +18,4 @@ Execution trace: TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
-Boogie program verifier finished with 0 verified, 1 error
+Boogie program verifier finished with 1 verified, 1 error
|