From 659491fddae2ee457100b6fa4c27afef3340621e Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 4 Apr 2012 18:40:59 -0700 Subject: Fixed bug with triply nested maps and polymorphism (reported as Item # 10218). --- Test/aitest9/TestIntervals.bpl | 16 ++++++++++++++++ Test/aitest9/answer | 2 +- 2 files changed, 17 insertions(+), 1 deletion(-) (limited to 'Test/aitest9') 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 = [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 -- cgit v1.2.3