diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-13 14:38:28 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-13 14:38:28 -0700 |
| commit | a3d7bd9b4a7b62cb0d8e4b0762d8db51c1548f1e (patch) | |
| tree | 7399c9f5e251cd3d5c2d1641cea1e1b4623466e8 /Test/test0 | |
| parent | 2178536246cab25a4564a15c05a6d2fcb4ac54ca (diff) | |
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.
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 13 | ||||
| -rw-r--r-- | Test/test0/SeparateVerification0.bpl | 21 | ||||
| -rw-r--r-- | Test/test0/SeparateVerification1.bpl | 19 | ||||
| -rw-r--r-- | Test/test0/runtest.bat | 9 |
4 files changed, 62 insertions, 0 deletions
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
|