Test/aitest0/constants.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

// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Test the constant propagation AI

var GlobalFlag : bool;

const A, B, C:int;		// Consts

procedure Join (b : bool)
  modifies GlobalFlag;
{  
  var x, y, z:int;
  
  start:
    GlobalFlag := true;
    x := 3;
    y := 4;
    z := x + y;
    goto Then, Else; // if (b)
 
  Then:
    assume b == true;
    x := x + 1;
    goto join;

  Else:
    assume b == false;
    y := 4;
    goto join;
    
  join:
    assert y == 4;
    assert z == 7;
    assert GlobalFlag == true;
    return;
}    


procedure Loop ()
{
  var c, i: int;

  start:
    c := 0; i := 0;
    goto test;
 
  test:
    // if (i < 10);
    goto Then, Else;

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

  Else:
    return;
}

procedure Evaluate () 
{
 var i : int;

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