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.

1 files changed, 19 insertions, 0 deletions

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

+}