blob: 622a0b36f95125727aa11e1087496116c1d3e3cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
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 = <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;
}
// -----
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
}
|
