From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/aitest9/TestIntervals.bpl | 144 ++++++++++++++++++++-------------------- Test/aitest9/VarMapFixpoint.bpl | 120 ++++++++++++++++----------------- 2 files changed, 132 insertions(+), 132 deletions(-) (limited to 'Test/aitest9') diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index 307a1da4..c9bb8284 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -1,72 +1,72 @@ -// RUN: %boogie "%s" -infer:j > "%t" -// RUN: %diff "%s.expect" "%t" -procedure P() -{ - var a: int, b: int, c: int; - - a := 0; - while (*) { - a := a + 1; - } - // a in [0, infty] - - b := 0; - if (*) { b := b + 1; } - if (*) { b := b + 1; } - if (*) { b := b + 1; } - // b in [0, 3] - - c := a - b; - // c in [-3, infty] - goto Next; - - Next: - 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; -} - -// ----- - -procedure Neq() -{ - var n: int; - assume 2 <= n && n <= 10; - assume 2 != n; - assume n != 10; - while (*) { - n := n; - } - assert 3 <= n; - assert n < 10; -} - -procedure NeqX() -{ - var n: real; - assume 2.0 <= n && n <= 10.0; - assume 2.0 != n; - assume n != 10.0; - // The following statement will cause Boogie to know about n only - // what the abstract interpreter has inferred so far. - while (*) { n := n; } - - assert 2.0 <= n && n <= 10.0; // yes - assert 2.0 < n; // error, the abstract domain is not precise enough to figure this out - assert n < 10.0; // error, ditto -} +// RUN: %boogie "%s" -infer:j > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P() +{ + var a: int, b: int, c: int; + + a := 0; + while (*) { + a := a + 1; + } + // a in [0, infty] + + b := 0; + if (*) { b := b + 1; } + if (*) { b := b + 1; } + if (*) { b := b + 1; } + // b in [0, 3] + + c := a - b; + // c in [-3, infty] + goto Next; + + Next: + 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; +} + +// ----- + +procedure Neq() +{ + var n: int; + assume 2 <= n && n <= 10; + assume 2 != n; + assume n != 10; + while (*) { + n := n; + } + assert 3 <= n; + assert n < 10; +} + +procedure NeqX() +{ + var n: real; + assume 2.0 <= n && n <= 10.0; + assume 2.0 != n; + assume n != 10.0; + // The following statement will cause Boogie to know about n only + // what the abstract interpreter has inferred so far. + while (*) { n := n; } + + assert 2.0 <= n && n <= 10.0; // yes + assert 2.0 < n; // error, the abstract domain is not precise enough to figure this out + assert n < 10.0; // error, ditto +} diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl index 6a051ed9..83ea45ca 100644 --- a/Test/aitest9/VarMapFixpoint.bpl +++ b/Test/aitest9/VarMapFixpoint.bpl @@ -1,60 +1,60 @@ -// RUN: %boogie "%s" -infer:j > "%t" -// RUN: %diff "%s.expect" "%t" -procedure main() -{ - var x: int, y: int, z: int; - - start: - x := 2; - y := 6; - goto LoopHead; - - LoopHead: - assert y < 10; // error: the loop body sets y to an arbitrary value - goto LoopBody, LoopEnd; - - LoopBody: - havoc y; - goto LoopHead; - - LoopEnd: - return; -} - -procedure SimpleWhile5() returns (returnValue: int) -{ - var i: int; - - start: - returnValue := 1; - havoc i; - goto LoopHead; - - LoopHead: - goto LoopBody, LoopEnd; - - LoopBody: - // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret - // assume commands, so we start a loop - i := 1; - goto IncLoopHead; - - IncLoopHead: - goto IncI, IncDone; - - IncI: - i := i + 1; - goto IncLoopHead; - - IncDone: - // now we have 1 <= i - assert 1 <= i; - - returnValue := returnValue * i; - i := i - 1; - goto LoopHead; - - LoopEnd: - assert returnValue >= 1; - return; -} +// RUN: %boogie "%s" -infer:j > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() +{ + var x: int, y: int, z: int; + + start: + x := 2; + y := 6; + goto LoopHead; + + LoopHead: + assert y < 10; // error: the loop body sets y to an arbitrary value + goto LoopBody, LoopEnd; + + LoopBody: + havoc y; + goto LoopHead; + + LoopEnd: + return; +} + +procedure SimpleWhile5() returns (returnValue: int) +{ + var i: int; + + start: + returnValue := 1; + havoc i; + goto LoopHead; + + LoopHead: + goto LoopBody, LoopEnd; + + LoopBody: + // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret + // assume commands, so we start a loop + i := 1; + goto IncLoopHead; + + IncLoopHead: + goto IncI, IncDone; + + IncI: + i := i + 1; + goto IncLoopHead; + + IncDone: + // now we have 1 <= i + assert 1 <= i; + + returnValue := returnValue * i; + i := i - 1; + goto LoopHead; + + LoopEnd: + assert returnValue >= 1; + return; +} -- cgit v1.2.3