Test/test2/Call.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

procedure Bar() returns (barresult: ref);

procedure Foo();

implementation Foo()
{
  var x: ref;

  entry:
    call x := Bar();
    assume x == null;
    call x := Bar();
    assert x == null;
    return;

}

procedure DifferentFormalNames(x: int, y: int) returns (z: int);
  requires x < y;
  ensures z == x;

implementation DifferentFormalNames(x: int, y: int) returns (z: int)
{
  start:
    assert x < y;
    z := x;
    return;
}

implementation DifferentFormalNames(y: int, x: int) returns (w: int)
{
  start:
    goto A, B;
  A:
    assert y < x;
    assume false;
    return;
  B:
    w := y;
    return;
}

implementation DifferentFormalNames(y: int, x: int) returns (w: int)
{
  start:
    assert x < y;  // error
    w := y;
    return;
}

implementation DifferentFormalNames(y: int, x: int) returns (w: int)
{
  start:
    w := x;
    return;  // error: postcondition violation
}

type ref;

const null : ref;