diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 |
1 files changed, 5 insertions, 0 deletions
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);
|