Test/aitest1/ineq.bpl


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
71
72
73
74
75
76
77
78
79
80
81
82
83

// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Test the polyhedra domain for linear inequalities


procedure SimpleLoop ()
{  
  var i : int;
  
  start:
    i := 0;
    goto test;
 
  test:
    goto Then, Else;

  Then:
    assume i < 10;
    i := i + 1;
    goto test;

  Else:
    assume ! (i < 10);
    return;
}    


procedure VariableBoundLoop (n : int)
{  
  var i : int;
  
  start:
    i := 0;
    goto test;
 
  test:
    goto Then, Else;

  Then:
    assume i < n;
    i := i + 1;
    goto test;

  Else:
    assume ! (i < n);
    return;
}    

procedure Foo () 
{
 var i : int;

 start:
 i := 3 * i + 1;
 i := 3 * (i + 1);
 i := 1 + 3 * i;
 i := (i + 1) * 3 ;
 return;
}

procedure FooToo () 
{
 var i : int;

 start:
 i := 5;
 i := 3 * i + 1;
 i := 3 * (i + 1);
 i := 1 + 3 * i;
 i := (i + 1) * 3 ;
 return;
}

procedure FooTooStepByStep () 
{
 var i : int;

 L0: i := 5; goto L1;
 L1: i := 3 * i + 1; goto L2;
 L2: i := 3 * (i + 1); goto L3;
 L3: i := 1 + 3 * i; goto L4;
 L4: i := (i + 1) * 3; return;
}