Test/test15/CaptureState.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

type Ref;
type FieldName;
var Heap: [Ref,FieldName]int;

const unique F: FieldName;

procedure P(this: Ref, x: int, y: int) returns (r: int)
  ensures 0 <= r;
{
  var m: int;

  assume {:captureState "top"} true;

  m := Heap[this, F];
  if (0 <= x) {
    assume {:captureState "then"} true;
    m := m + 1;
    assume {:captureState "postUpdate0"} true;
  } else {
    assume {:captureState "else"} true;
    m := (m + y) * (m + y);
    assume {:captureState "postUpdate1"} true;
  }
  r := m + m;
  assume {:captureState "end"} true;
}