Add support for the "include" keyword, which accepts a (possibly relative) path

to another Dafny file.  That file's functions and methods are included but not checked.
This is intended to support incremental verification on a per-file basis.

1 files changed, 12 insertions, 0 deletions

diff --git a/Test/dafny0/Include.dfy b/Test/dafny0/Include.dfy
new file mode 100644
index 00000000..a228194f
--- /dev/null
+++ b/Test/dafny0/Include.dfy
@@ -0,0 +1,12 @@
+

+include "Includee.dfy"

+

+method test_include(z:int)

+{

+  // Make sure we can still see function bodies

+  assert forall y :: f(y) == 2*y;

+

+  // Use an unverified method

+  var w := m_unproven(z);

+  assert w == 2*z;

+}