diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 20 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 |
2 files changed, 17 insertions, 8 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 802b1918..9a898cbe 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -354,10 +354,10 @@ namespace Microsoft.Dafny /// AutoContracts will then:
///
/// Declare:
- /// ghost var Repr: set(object);
+ /// ghost var Repr: set(object)
///
/// For function/predicate Valid(), insert:
- /// reads this, Repr;
+ /// reads this, Repr
/// Into body of Valid(), insert (at the beginning of the body):
/// this in Repr && null !in Repr
/// and also insert, for every array-valued field A declared in the class:
@@ -369,19 +369,23 @@ namespace Microsoft.Dafny ///
/// For every constructor, add:
/// modifies this;
- /// ensures Valid() && fresh(Repr - {this});
+ /// ensures Valid() && fresh(Repr - {this})
/// At the end of the body of the constructor, add:
/// Repr := {this};
/// if (A != null) { Repr := Repr + {A}; }
/// if (F != null) { Repr := Repr + {F} + F.Repr; }
///
- /// For every method, add:
- /// requires Valid();
- /// modifies Repr;
- /// ensures Valid() && fresh(Repr - old(Repr));
+ /// For every non-static non-ghost method that is not a "simple query method",
+ /// add:
+ /// requires Valid()
+ /// modifies Repr
+ /// ensures Valid() && fresh(Repr - old(Repr))
/// At the end of the body of the method, add:
/// if (A != null) { Repr := Repr + {A}; }
/// if (F != null) { Repr := Repr + {F} + F.Repr; }
+ /// For every non-static method that is either ghost or is a "simple query method",
+ /// add:
+ /// requires Valid()
/// </summary>
public class AutoContractsRewriter : IRewriter
{
@@ -566,7 +570,7 @@ namespace Microsoft.Dafny AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
}
- } else if (member is Method && !member.IsStatic) {
+ } else if (member is Method && !member.IsStatic && !member.IsGhost) {
var m = (Method)member;
if (Valid != null && !IsSimpleQueryMethod(m)) {
if (member.RefinementBase == null) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 37408aa1..a1fbe646 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);
|