summaryrefslogtreecommitdiff
path: root/Test/aitest0/Answer
blob: 587504602aecff2bf755aec3f8dfaf5d32a2f3d7 (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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
var GlobalFlag: bool;

const A: int;

const B: int;

const C: int;

procedure Join(b: bool);
  modifies GlobalFlag;



implementation Join(b: bool)
{
  var x: int;
  var y: int;
  var z: int;

  start:
    assume true;
    GlobalFlag := true;
    x := 3;
    y := 4;
    z := x + y;
    assume x == 3 && y == 4 && z == 7;
    goto Then, Else;

  Then:
    assume x == 3 && y == 4 && z == 7;
    assume b <==> true;
    x := x + 1;
    assume x == 4 && y == 4 && z == 7;
    goto join;

  Else:
    assume x == 3 && y == 4 && z == 7;
    assume b <==> false;
    y := 4;
    assume x == 3 && y == 4 && z == 7;
    goto join;

  join:
    assume y == 4 && z == 7;
    assert y == 4;
    assert z == 7;
    assert GlobalFlag <==> true;
    assume y == 4 && z == 7;
    return;
}



procedure Loop();



implementation Loop()
{
  var c: int;
  var i: int;

  start:
    assume true;
    c := 0;
    i := 0;
    assume c == 0 && i == 0;
    goto test;

  test:  // cut point
    assume c == 0;
    assume c == 0;
    goto Then, Else;

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

  Else:
    assume c == 0;
    assume c == 0;
    return;
}



procedure Evaluate();



implementation Evaluate()
{
  var i: int;

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



Boogie program verifier finished with 0 verified, 0 errors