diff options
Diffstat (limited to 'Test/test0/SeparateVerification0.bpl')
-rw-r--r-- | Test/test0/SeparateVerification0.bpl | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl index a5c3962a..93324437 100644 --- a/Test/test0/SeparateVerification0.bpl +++ b/Test/test0/SeparateVerification0.bpl @@ -1,27 +1,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);
+// 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); |