Added support for verifying Dafny program snapshots from the command-line.

5 files changed, 30 insertions, 0 deletions

diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy
new file mode 100644
index 00000000..73db9f9c
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v0.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures false;

diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy
new file mode 100644
index 00000000..28f9f283
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures true;

diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg
new file mode 100644
index 00000000..07cb869f
--- /dev/null
+++ b/Test/dafny0/snapshots/lit.local.cfg
@@ -0,0 +1,5 @@
+# This test is unusual in that we don't use the .bpl files
+# directly on the command line. So instead we'll invoke
+# files in this directory with extension '.snapshot'. There
+# will only be one for now
+config.suffixes = ['.snapshot']
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
new file mode 100644
index 00000000..6d2f880f
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
new file mode 100644
index 00000000..7906e7a5
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 3 verified, 0 errors

+Snapshots0.v1.dfy(4,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 1 error