Test/codeexpr/CodeExpr0.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

procedure P()
{
  assert |{ A: return true; }|;
}

// ------------

procedure Q()
{
  assert |{ var x: bool; A: x := true; return x; }|;
}

procedure R()
{
  assert |{ var x: bool; A: x := false; return x; }|;  // error
}

procedure S()
{
  assert |{ var x: bool; A: return x; }|;  // error
}

// ------------

procedure T(x: int, y: int)
  requires |{ var z: bool;
              Start: goto A;
              A: z := false; goto B, C;
              B: assume 0 <= x; goto D;
              C: assume x < 0; goto R;
              D: goto E, F;
              E: assume 0 <= y; z := true; goto R;
              F: assume y < 0; goto R;
              R: return z;
           }|;
{
  assert 0 <= x + y;
}

procedure U(x: int, y: int)
  requires |{ var z: bool;
              Start: goto A;
              A: z := false; goto B, C;
              B: assume 0 <= x; goto D;
              C: assume x < 0; goto R;
              D: goto E, F;
              E: assume 0 <= y; z := true; goto R;
              F: assume y < 0; goto R;
              R: return z;
           }|;
{
  assert x <= y;  // error
}