From bebfbaa98ac099cba47cfd1f02e6781ea257997f Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 3 Jul 2014 03:22:45 +0200
Subject: Changed "dummy" checksums to "stable" and added more tests for the
 verification result caching.

---
 Source/Dafny/Translator.cs                    |  4 ++--
 Test/dafny0/snapshots/Snapshots0.v1.dfy       |  2 +-
 Test/dafny0/snapshots/Snapshots1.v0.dfy       | 13 +++++++++++++
 Test/dafny0/snapshots/Snapshots1.v1.dfy       | 13 +++++++++++++
 Test/dafny0/snapshots/Snapshots2.v0.dfy       | 19 +++++++++++++++++++
 Test/dafny0/snapshots/Snapshots2.v1.dfy       | 19 +++++++++++++++++++
 Test/dafny0/snapshots/runtest.snapshot        |  2 +-
 Test/dafny0/snapshots/runtest.snapshot.expect | 20 ++++++++++++++++++++
 8 files changed, 88 insertions(+), 4 deletions(-)
 create mode 100644 Test/dafny0/snapshots/Snapshots1.v0.dfy
 create mode 100644 Test/dafny0/snapshots/Snapshots1.v1.dfy
 create mode 100644 Test/dafny0/snapshots/Snapshots2.v0.dfy
 create mode 100644 Test/dafny0/snapshots/Snapshots2.v1.dfy

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 39b1ea95..854883c8 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -398,13 +398,13 @@ namespace Microsoft.Dafny {
           var impl = decl as Implementation;
           if (impl != null && impl.FindStringAttribute("checksum") == null)
           {
-            impl.AddAttribute("checksum", "dummy");
+            impl.AddAttribute("checksum", "stable");
           }
 
           var func = decl as Bpl.Function;
           if (func != null && func.FindStringAttribute("checksum") == null)
           {
-            func.AddAttribute("checksum", "dummy");
+            func.AddAttribute("checksum", "stable");
           }
         }
       }
diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy
index 28f9f283..db9fc01a 100644
--- a/Test/dafny0/snapshots/Snapshots0.v1.dfy
+++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy
@@ -1,7 +1,7 @@
 method foo()
 {
   bar();
-  assert false;
+  assert false;  // error
 }
 
 method bar()
diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy
new file mode 100644
index 00000000..dd1e7deb
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots1.v0.dfy
@@ -0,0 +1,13 @@
+method M()
+{
+  N();
+  assert false;
+}
+
+method N()
+  ensures P;
+
+predicate P
+{
+  false
+}
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy
new file mode 100644
index 00000000..93ad6068
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy
@@ -0,0 +1,13 @@
+method M()
+{
+  N();
+  assert false;  // error
+}
+
+method N()
+  ensures P;
+
+predicate P
+{
+  true
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy
new file mode 100644
index 00000000..37b9982b
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots2.v0.dfy
@@ -0,0 +1,19 @@
+method M()
+{
+  N();
+  assert false;
+}
+
+method N()
+  ensures P;
+
+predicate P
+  ensures P == Q;
+
+predicate Q
+  ensures Q == R;
+
+predicate R
+{
+  false
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy
new file mode 100644
index 00000000..03719744
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots2.v1.dfy
@@ -0,0 +1,19 @@
+method M()
+{
+  N();
+  assert false;  // error
+}
+
+method N()
+  ensures P;
+
+predicate P
+  ensures P == Q;
+
+predicate Q
+  ensures Q == R;
+
+predicate R
+{
+  true
+}
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
index 6d2f880f..c3cf6b00 100644
--- a/Test/dafny0/snapshots/runtest.snapshot
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 7906e7a5..87827811 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,7 +1,27 @@
 
+-------------------- Snapshots0.dfy --------------------
+
 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
+
+-------------------- Snapshots1.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+Snapshots1.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
+
+-------------------- Snapshots2.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+Snapshots2.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 5 verified, 1 error
-- 
cgit v1.2.3