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

// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type {:sourcefile "test.ssc"} T; 

function {:source "test.scc"} f(int) returns (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, any, name;


// allow \" and other backslashes rather liberally:

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

const again: int;