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

var g: int;

procedure Foo() returns ();
    modifies g;
    free ensures 0 <= g;

implementation Foo() returns ()
{
    entry:
        g := g + 1;
        return;
}

procedure BarGood() returns ()
    modifies g;
{
    entry:
        call Foo();
        assert 0 <= g;
        return;
}

procedure BarBad() returns ()
    modifies g;
{
    entry:
        call Foo();
        assert 0 < g;
        return;
}

// ----- Free preconditions

procedure Proc() returns ();
    free requires g == 15;

implementation Proc() returns ()
{
    entry:
        assert g > 10;  // yes, this condition can be used here
        return;
}

implementation Proc() returns ()
{
    entry:
        assert g < 10;  // error
        return;
}

procedure Caller0() returns ()
{
    entry:
        call Proc();  // yes, legal, since the precondition is not checked
        return;
}

procedure Caller1() returns ()
{
    entry:
        call Proc();
        assert g > 10;  // error, because:
        // Free preconditions are ignored (that is, treated as "skip") for the caller.
        // This is a BoogiePL design choice.  Another alternative would be to treat free
        // preconditions as assume commands also on the caller side, either in the order
        // that all preconditions are given, or before or after all the checked preconditions
        // have been checked.
        return;
}