summaryrefslogtreecommitdiff
path: root/Test/test0/SeparateVerification1.bpl
blob: 0e3e7926f3668f2a54d383c0a5ea156bf46d2407 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// to be used with SeparateVerification0.bpl

// x and y are declared in SeparateVerification0.bpl
axiom x + y <= 100;

// these are declared as :extern as SeparateVerification0.bpl
type T;
const C: int;
function F(): int;
var n: int;
procedure P();
procedure {:extern} Q(x: int);

procedure Main() {
  call P();  // note, calling the parameter-less non-extern P (an extern and a non-extern
             // declaration of the same name are usually mostly identical declarations,
             // but Boogie allows them to be different, because it ignores the extern ones)
  call Q();  // ditto
}