summaryrefslogtreecommitdiff
path: root/Test/test0/SeparateVerification0.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/SeparateVerification0.bpl')
-rw-r--r--Test/test0/SeparateVerification0.bpl54
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);