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

// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// inlined functions

function Twice(x: int) returns (int)
{
  x + x
}

function {:inline} Double(x: int) returns (int)
{
  3 * x - x
}

function f(int) returns (int);
function g(int) returns (int);
function h(int) returns (int);
function k(int) returns (int);
axiom (forall x: int :: Twice(x) == f(x));  // here, Twice(x) and f(x) are both triggers
axiom (forall x: int :: Double(x) == g(x));  // since Double is inlined, the trigger here is just g(x)
axiom (forall x: int :: { f(x) } f(x) < h(x) );
axiom (forall x: int :: { g(x) } g(x) < k(x) );

procedure P(a: int, b: int, c: int)
{
  // The following is provable, because Twice triggers its definition and the resulting f(a)
  // triggers the relation to h(a).
  assert Twice(a) < h(a);
  if (*) {
    // The following is NOT provable, because Double is inlined and thus no g(b) term is ever
    // created
    assert Double(b) < k(b);  // error
  } else {
    // The following IS provable, because the explicit g(c) will cause both of the necessary
    // quantifiers to trigger
    assert g(c) == 2*c;
    assert Double(c) < k(c);
  }
}

// nullary functions

function Five() returns (int) { 5 }

function {:inline} Eight() returns (e: int) { 8 }

procedure Q()
{
  assert 8 * Five() == 5 * Eight();
}