summaryrefslogtreecommitdiff
path: root/Test/aitest9/TestIntervals.bpl
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
}