From a3d7bd9b4a7b62cb0d8e4b0762d8db51c1548f1e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 13 May 2011 14:38:28 -0700
Subject: Boogie: added features to help with modular verification. In
 particular, define FILE_n when parsing file n on the command line, and
 support :extern and :ignore attributes on top-level declarations.

---
 Test/test0/Answer                    | 13 +++++++++++++
 Test/test0/SeparateVerification0.bpl | 21 +++++++++++++++++++++
 Test/test0/SeparateVerification1.bpl | 19 +++++++++++++++++++
 Test/test0/runtest.bat               |  9 +++++++++
 4 files changed, 62 insertions(+)
 create mode 100644 Test/test0/SeparateVerification0.bpl
 create mode 100644 Test/test0/SeparateVerification1.bpl

(limited to 'Test/test0')

diff --git a/Test/test0/Answer b/Test/test0/Answer
index 0441b69b..d434a8ca 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -247,3 +247,16 @@ BadQuantifier.bpl(3,15): error: invalid QuantifierBody
 EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a
 EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a
 2 name resolution errors detected in EmptyCallArgs.bpl
+----- SeparateVerification0.bpl
+SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
+1 name resolution errors detected in SeparateVerification0.bpl
+----- SeparateVerification1.bpl SeparateVerification0.bpl
+SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
+2 name resolution errors detected in SeparateVerification0.bpl
+----- SeparateVerification0.bpl SeparateVerification0.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
+----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl
new file mode 100644
index 00000000..5a8ef283
--- /dev/null
+++ b/Test/test0/SeparateVerification0.bpl
@@ -0,0 +1,21 @@
+// 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);
diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl
new file mode 100644
index 00000000..0e3e7926
--- /dev/null
+++ b/Test/test0/SeparateVerification1.bpl
@@ -0,0 +1,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
+}
diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat
index c7c6ee3d..5ecc22dc 100644
--- a/Test/test0/runtest.bat
+++ b/Test/test0/runtest.bat
@@ -31,3 +31,12 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify Orderings.bpl
 %BGEXE% %* /noVerify BadQuantifier.bpl
 %BGEXE% %* /noVerify EmptyCallArgs.bpl
+
+echo ----- SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl
+echo ----- SeparateVerification1.bpl SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification1.bpl SeparateVerification0.bpl
+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl
+echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
+%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
-- 
cgit v1.2.3