Test/test0/AttributeResolution.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 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type {:sourcefile foo} T; 

function {:source bar} f(int) returns (int);

const {:description baz} unique MAXINT: int;

axiom {:naming qux} (forall i: int :: {f(ij)} f(i) == i+1);

var {:description mux} $Heap: [ref, int]bool;

var {:sort_of_like_a_trigger fux} Bla: [ref, int]bool;

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

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

// ------  and here are various correct things


const {:Correct hux0 + F(hux1)} hux0: int;

function {:Correct F(hux0) + hux1} F(int) returns (int);

axiom {:Correct F(hux0 + hux1)} true;

var {:Correct hux0*hux1} hux1: int;

procedure {:Correct hux0 - hux1} P();

implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} P()
{
}

type ref;