From 351bce8912c2ae2159abb0ebe2b1e1ad1a4b4290 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 27 Nov 2015 17:57:47 -0800
Subject: Make cached results dependent on if a function is ghost or not

---
 Source/Dafny/Translator.cs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 8e8c3c19..e3915e6d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3510,10 +3510,13 @@ namespace Microsoft.Dafny {
 
     private void InsertChecksum(Function f, Bpl.Declaration decl, bool specificationOnly = false)
     {
+      Contract.Requires(f != null);
+      Contract.Requires(decl != null);
       byte[] data;
       using (var writer = new System.IO.StringWriter())
       {
         var printer = new Printer(writer);
+        writer.Write(f.IsGhost ? "function" : "function method");
         printer.PrintAttributes(f.Attributes);
         printer.PrintFormals(f.Formals);
         writer.Write(": ");
@@ -3534,6 +3537,8 @@ namespace Microsoft.Dafny {
 
     private void InsertChecksum(Bpl.Declaration decl, byte[] data)
     {
+      Contract.Requires(decl != null);
+      Contract.Requires(data != null);
       var md5 = System.Security.Cryptography.MD5.Create();
       var hashedData = md5.ComputeHash(data);
       var checksum = BitConverter.ToString(hashedData);
-- 
cgit v1.2.3