Test/test0/WhereResolution.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

type double;

function R(int) returns (bool);
function K(double, bool) returns (bool);

var y: int where R(y);
var g: int where h ==> g == 12;
var h: bool where g < 100;
var k: double where K(k, h);

procedure P(x: int where x > 0) returns (y: int where y < 0);
  requires x < 100;
  modifies g;
  ensures -100 < y;

implementation P(xx: int) returns (yy: int)
{
  var a: int where a == 10;
  var b: int where a == b && b < g;

  start:
    a := xx;
    call b := P(a);
    yy := b;
    return;
}

procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
    returns (v: bool where v,
             y: int where x + y + z < 0,
             z: int where g == 12,
             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause
             beta: ref where (forall r: ref :: r == beta ==> beta == null))
  requires x < 100;
  modifies g;
  ensures -100 < y;
{
  var a: int;
  var b: int;

  start:
    a := x;
    call b := P(a);
    y := b;
    return;
}

const SomeConstant: ref;

procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
{
  var m: ref where m != SomeConstant;
  var k: int where k != SomeConstant;
  var r: ref where (forall abc: ref :: abc == SomeConstant);
  var b: bool;
  start:
    b := (forall l: ref :: l == SomeConstant);
    return;
}

type ref;
const null : ref;