Test/test0/Quoting.bpl.expect


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


function \true() : bool;

type \procedure;

procedure \old(any: \procedure) returns (\var: \procedure);


implementation \old(any: \procedure) returns (\var: \procedure)
{
  var \modifies: \procedure;

    \modifies := any;
    \var := \modifies;
}


procedure qux(a: \procedure);


implementation qux(a: \procedure)
{
  var \var: \procedure;
  var x: bool;

    call \var := \old(a);
    x := \true();
}


Boogie program verifier finished with 0 verified, 0 errors