Test/test0/AttributeParsing.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
36
37
38
39
40
41
42
43
44
45
46


type {:sourcefile "test.ssc"} T;

function {:source "test.scc"} f(int) : int;

const {:description "The largest integer value"} unique MAXINT: int;

axiom {:naming "MyFavoriteAxiom"} (forall i: int :: { f(i) } f(i) == i + 1);

var {:description "memory"} $Heap: [ref,name]any;

var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref,name]any;

procedure {:use_impl 1} foo(x: int) returns (n: int);


implementation {:id 1} foo(x: int) returns (n: int)
{
  block1:
    return;
}


implementation {:id 2} foo(x: int) returns (n: int)
{
  block1:
    return;
}


type ref;

type any;

type name;

procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();


const again: int;

Boogie program verifier finished with 0 verified, 0 errors