blob: 4115c4b02a4c9c184b03e12b9b3db681170791fb (
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
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure P() returns (x, y: int)
ensures x == y; // ensured by the body
ensures x == 0; // error: not ensured by the body
ensures y == 0; // follows from the previous two ensures clauses (provided they are
// indeed evaluated in this order, which they are supposed to be)
{
x := y;
}
procedure Q() returns (x, y: int)
{
x := y;
assert x == y; // ensured by the body
assert x == 0; // error: not ensured by the body
assert y == 0; // follows from the previous two asserts (provided they are
// indeed evaluated in this order, which they are supposed to be)
}
procedure R()
{
var a, b: int;
a := b;
call S(a, b);
}
procedure S(x, y: int)
// In the call from R:
requires x == y; // ensured by the body of R
requires x == 0; // error: not ensured by the body of R
requires y == 0; // follows from the previous two requires clauses (provided they are
// indeed evaluated in this order, which they are supposed to be)
{
}
|