Dafny:

* Added DeclType(f)==C axioms, which for each field f says which class declares it.

Boogie:
* Changed behavior of free loop invariants.  Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures.  The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE:  I did NOT yet make the corresponding change for loop unrolling, but it is needed.

2 files changed, 11 insertions, 1 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index fa0d1529..9ff60f1b 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -181,6 +181,8 @@ const unique #loc.$Heap: $token;
 

 const unique alloc: Field bool;

 

+function DeclType<T>(Field T) returns (ClassName);

+

 function $HeapSucc(HeapType, HeapType) returns (bool);

 axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

   $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 15f208f0..1cac78af 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -909,7 +909,7 @@ namespace Microsoft.Dafny {
     }

     

     Bpl.Constant! GetField(Field! f)

-      requires predef != null;

+      requires sink != null && predef != null;

     {

       Bpl.Constant fc;

       if (fields.TryGetValue(f, out fc)) {

@@ -918,6 +918,9 @@ namespace Microsoft.Dafny {
         Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));

         fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);

         fields.Add(f, fc);

+        // axiom DeclType(f) == C;

+        Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass))));

+        sink.TopLevelDeclarations.Add(ax);

       }

       return fc;

     }

@@ -2243,6 +2246,7 @@ namespace Microsoft.Dafny {
       DynamicType,  // allocated type

       TypeParams,   // type parameters to allocated type

       TypeTuple,

+      DeclType,

       

       // CEV

       CevInit,

@@ -2364,6 +2368,10 @@ namespace Microsoft.Dafny {
           assert args.Length == 2;

           assert typeInstantiation == null;

           return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args);

+        case BuiltinFunction.DeclType:

+          assert args.Length == 1;

+          assert typeInstantiation != null;

+          return FunctionCall(tok, "DeclType", predef.ClassNameType, args);

           

         case BuiltinFunction.CevInit:

           assert args.Length == 1;