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

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)
{
}