blob: a5c3962a19f0c274778f8faaa73e4030eea4a42b (
plain)
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
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// RUN: %boogie -noVerify "%s" "%s" > "%t"
// RUN: %diff NoErrors.expect "%t"
// RUN: %boogie -noVerify "%s" "%s" SeparateVerification1.bpl > "%t"
// RUN: %diff NoErrors.expect "%t"
// need to include this file twice for it to include all necessary declarations
#if FILE_0
const x: int;
#else
const y: int;
#endif
#if FILE_1
axiom x == 12;
procedure Q();
#else
axiom y == 7;
#endif
// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's)
type {:extern} T;
const {:extern} C: int;
function {:extern} F(): int;
var {:extern} n: int;
procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int);
|
