Merge

12 files changed, 204 insertions, 249 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 4eeedcbf..7c8536a3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -182,7 +182,7 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl
     { Attribute<ref attrs> }

     NoUSIdent<out id>                          

     ((

-      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); .)

+      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .)

        "{"                                       (. module.BodyStartTok = t; .)

         { (. isGhost = false; .)

           [ "ghost"  (. isGhost = true; .) ]

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index df6fc2a6..032891ce 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny {
 

   public class BuiltIns

   {

-    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null);

+    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);

     Dictionary<int, ClassDecl/*!*/> arrayTypeDecls = new Dictionary<int, ClassDecl>();

     public readonly ClassDecl ObjectDecl;

     public BuiltIns() {

@@ -840,6 +840,7 @@ namespace Microsoft.Dafny {
     

     public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();

     public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();

+    public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();

     public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.

                                        // it is abstract). Otherwise, it points to that definition.

     public ModuleSignature Refines;

@@ -868,14 +869,14 @@ namespace Microsoft.Dafny {
     public int Height;  // height in the topological sorting of modules; filled in during resolution

     public readonly bool IsGhost;

     public readonly bool IsAbstract; // True iff this module represents an abstract interface

-

+    private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TopLevelDecls));

       Contract.Invariant(CallGraph != null);

     }

 

-    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase,  Attributes attributes)

+    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase,  Attributes attributes, bool isBuiltinName)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -884,6 +885,7 @@ namespace Microsoft.Dafny {
       IsAbstract = isAbstract;

       RefinementBaseRoot = null;

       RefinementBase = null;

+      IsBuiltinName = isBuiltinName;

     }

     public virtual bool IsDefaultModule {

       get {

@@ -894,7 +896,10 @@ namespace Microsoft.Dafny {
     new public string CompileName {

       get {

         if (compileName == null) {

-          compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);

+          if (IsBuiltinName)

+            compileName = Name;

+          else

+            compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);

         }

         return compileName;

       }

@@ -916,7 +921,7 @@ namespace Microsoft.Dafny {
   }

 

   public class DefaultModuleDecl : ModuleDefinition {

-    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null) {

+    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, false) {

     }

     public override bool IsDefaultModule {

       get {

@@ -1093,7 +1098,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(EnclosingDatatype != null);

         Contract.Ensures(Contract.Result<string>() != null);

 

-        return "#" + EnclosingDatatype.FullName + "." + Name;

+        return "#" + EnclosingDatatype.FullCompileName + "." + Name;

       }

     }

   }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 5f4c1bf4..f82f5e88 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -249,7 +249,7 @@ bool IsAttribute() {
 				Get();

 				QualifiedName(out idRefined);

 			}

-			module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); 

+			module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); 

 			Expect(6);

 			module.BodyStartTok = t; 

 			while (StartOf(1)) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9ab89223..325745f0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -97,6 +97,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();

     readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();

     readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();

+    ModuleSignature systemNameInfo = null;

     public Resolver(Program prog) {

       Contract.Requires(prog != null);

       builtIns = prog.BuiltIns;

@@ -142,7 +143,7 @@ namespace Microsoft.Dafny {
       var refinementTransformer = new RefinementTransformer(this);

       

       IRewriter rewriter = new AutoContractsRewriter();

-      var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

+      systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

       foreach (var decl in sortedDecls) {

         if (decl is LiteralModuleDecl) {

           // The declaration is a literal module, so it has members and such that we need

@@ -171,14 +172,9 @@ namespace Microsoft.Dafny {
           }

           literalDecl.Signature = RegisterTopLevelDecls(m);

           literalDecl.Signature.Refines = refinedSig;

+          var sig = literalDecl.Signature;

           // set up environment

-          moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo);

-          // resolve

-          var datatypeDependencies = new Graph<IndDatatypeDecl>();

-          int prevErrorCount = ErrorCount;

-          ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

-          if (ErrorCount == prevErrorCount)

-          ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+          ResolveModuleDefinition(m, sig);

 

           refinementTransformer.PostResolve(m);

           // give rewriter a chance to do processing

@@ -194,16 +190,11 @@ namespace Microsoft.Dafny {
           }

         } else if (decl is AbstractModuleDecl) {

           var abs = (AbstractModuleDecl)decl;

-          ModuleSignature p; ModuleDefinition mod;

+          ModuleSignature p;

           if (ResolvePath(abs.Root, abs.Path, out p)) {

-            abs.Signature = MakeAbstractSignature(p, abs.Name, abs.Height, out mod);

+            abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules);

             abs.OriginalSignature = p;

-            moduleInfo = MergeSignature(abs.Signature, systemNameInfo);

             // resolve

-            var datatypeDependencies = new Graph<IndDatatypeDecl>();

-            ResolveTopLevelDecls_Signatures(mod.TopLevelDecls, datatypeDependencies);

-            ResolveTopLevelDecls_Meat(mod.TopLevelDecls, datatypeDependencies);

-            prog.Modules.Add(mod);

           } else {

             abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature

           }

@@ -224,6 +215,16 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {

+      moduleInfo = MergeSignature(sig, systemNameInfo);

+      // resolve

+      var datatypeDependencies = new Graph<IndDatatypeDecl>();

+      int prevErrorCount = ErrorCount;

+      ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

+      if (ErrorCount == prevErrorCount)

+        ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+    }

+

 

     public class ModuleBindings {

       private ModuleBindings parent;

@@ -355,6 +356,10 @@ namespace Microsoft.Dafny {
       foreach (var kv in m.Ctors) {

         info.Ctors[kv.Key] = kv.Value;

       }

+      foreach (var kv in m.StaticMembers) {

+        info.StaticMembers[kv.Key] = kv.Value;

+      }

+

       return info;

     }

     ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {

@@ -395,7 +400,13 @@ namespace Microsoft.Dafny {
             }

           }

           cl.HasConstructor = hasConstructor;

-

+          if (cl.IsDefaultClass) {

+            foreach (MemberDecl m in cl.Members) {

+              if (!sig.StaticMembers.ContainsKey(m.Name) && m.IsStatic && (m is Function || m is Method)) {

+                sig.StaticMembers.Add(m.Name, m);

+              }

+            }

+          }

         } else {

           DatatypeDecl dt = (DatatypeDecl)d;

 

@@ -453,17 +464,19 @@ namespace Microsoft.Dafny {
       return sig;

     }

 

-    private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, out ModuleDefinition mod) {

-      mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null);

+    private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> mods) {

+      var mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null, false);

       mod.Height = Height;

       foreach (var kv in p.TopLevels) {

-        mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod));

+        mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));

       }

       var sig = RegisterTopLevelDecls(mod);

       sig.Refines = p.Refines;

+      mods.Add(mod);

+      ResolveModuleDefinition(mod, sig);

       return sig;

     }

-    TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {

+    TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List<ModuleDefinition> mods, string Name) {

       Contract.Requires(d != null);

       Contract.Requires(m != null);

 

@@ -486,8 +499,9 @@ namespace Microsoft.Dafny {
         var dd = (ClassDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var mm = dd.Members.ConvertAll(CloneMember);

-        var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);

-        return cl;

+        if (dd is DefaultClassDecl) {

+          return new DefaultClassDecl(m, mm);

+        } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null); 

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

           return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);

@@ -497,9 +511,17 @@ namespace Microsoft.Dafny {
           alias.ModuleReference = a.ModuleReference;

           alias.Signature = a.Signature;

           return alias;

+        } else if (d is AbstractModuleDecl) {

+          var abs = (AbstractModuleDecl)d;

+          var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);

+          var a = new AbstractModuleDecl(abs.Path, abs.tok, m);

+          a.Signature = sig;

+          a.OriginalSignature = abs.OriginalSignature;

+          return a;

+        } else {

+          Contract.Assert(false);  // unexpected declaration

+          return null;  // to please compiler

         }

-        Contract.Assert(false);  // unexpected declaration

-        return null;  // to please compiler

       } else {

         Contract.Assert(false);  // unexpected declaration

         return null;  // to please compiler

@@ -4473,9 +4495,9 @@ namespace Microsoft.Dafny {
       //       (if two imported types have the same name, an error message is produced here)

       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

       //  - imported module name

-      //  - field name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

-      // Note, at present, modules do not give rise to new namespaces, which is something that should

-      // be changed in the language when modules are given more attention.

+      //  - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

+      //  - static function or method in the enclosing module.

+      

       Expression r = null;  // resolved version of e

       CallRhs call = null;

 

@@ -4537,18 +4559,20 @@ namespace Microsoft.Dafny {
           }

         }

 

-      } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) {

+      } else if ((classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))

+                 || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

         // ----- field, function, or method

         Expression receiver;

         if (member.IsStatic) {

-          receiver = new StaticReceiverExpr(id, currentClass);

+          receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

         } else {

           if (!scope.AllowInstance) {

             Error(id, "'this' is not allowed in a 'static' context");

             // nevertheless, set "receiver" to a value so we can continue resolution

           }

           receiver = new ImplicitThisExpr(id);

-          receiver.Type = GetThisType(id, currentClass);  // resolve here

+          receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass);  // resolve here

         }

         r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);

 

@@ -4569,10 +4593,11 @@ namespace Microsoft.Dafny {
       return call;

     }

 

-    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature info, bool twoState, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, bool allowMethodCall) {

       // Look up "id" as follows:

       //  - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)

       //       (if two imported types have the same name, an error message is produced here)

+      //  - static function or method of sig.

       // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but

       // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.

       Contract.Requires(p < e.Tokens.Count);

@@ -4580,8 +4605,9 @@ namespace Microsoft.Dafny {
       CallRhs call = null;

 

       TopLevelDecl decl;

+      MemberDecl member;

       var id = e.Tokens[p];

-      if (info.TopLevels.TryGetValue(id.val, out decl)) {

+      if (sig.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

           Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());

         } else if (decl is ClassDecl) {

@@ -4605,6 +4631,14 @@ namespace Microsoft.Dafny {
             r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);

           }

         }

+      } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

+        // ----- function, or method

+        Expression receiver;

+        Contract.Assert(member.IsStatic);

+        receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

+        r = ResolveSuffix(receiver, e, p, twoState, allowMethodCall, out call);

+

       } else {

         Error(id, "unresolved identifier: {0}", id.val);

         // resolve arguments, if any

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2cb54115..f50cae64 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -26,6 +26,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();

+    readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();

     Program program;

 

     [ContractInvariantMethod]

@@ -53,6 +54,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type HeapType;

       public readonly string HeapVarName;

       public readonly Bpl.Type ClassNameType;

+      public readonly Bpl.Type NameFamilyType;

       public readonly Bpl.Type DatatypeType;

       public readonly Bpl.Type DtCtorId;

       public readonly Bpl.Expr Null;

@@ -71,6 +73,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(HeapType != null);

         Contract.Invariant(HeapVarName != null);

         Contract.Invariant(ClassNameType != null);

+        Contract.Invariant(NameFamilyType != null);

         Contract.Invariant(DatatypeType != null);

         Contract.Invariant(DtCtorId != null);

         Contract.Invariant(Null != null);

@@ -126,7 +129,7 @@ namespace Microsoft.Dafny {
 

       public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,

                              Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

-                             Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,

+                             Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,

                              Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,

                              Bpl.Constant allocField, Bpl.Constant classDotArray) {

         #region Non-null preconditions on parameters

@@ -158,6 +161,7 @@ namespace Microsoft.Dafny {
         this.HeapType = heap.TypedIdent.Type;

         this.HeapVarName = heap.Name;

         this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());

+        this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new Bpl.TypeSeq());

         this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());

         this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());

         this.allocField = allocField;

@@ -180,6 +184,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeCtorDecl seqTypeCtor = null;

       Bpl.TypeCtorDecl fieldNameType = null;

       Bpl.TypeCtorDecl classNameType = null;

+      Bpl.TypeCtorDecl nameFamilyType = null;

       Bpl.TypeCtorDecl datatypeType = null;

       Bpl.TypeCtorDecl dtCtorId = null;

       Bpl.TypeCtorDecl boxType = null;

@@ -203,6 +208,8 @@ namespace Microsoft.Dafny {
             dtCtorId = dt;

           } else if (dt.Name == "ref") {

             refType = dt;

+          } else if (dt.Name == "NameFamily") {

+            nameFamilyType = dt;

           } else if (dt.Name == "BoxType") {

             boxType = dt;

           } else if (dt.Name == "TickType") {

@@ -250,6 +257,8 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");

       } else if (classNameType == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");

+      } else if (nameFamilyType == null) {

+        Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily");

       } else if (datatypeType == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");

       } else if (dtCtorId == null) {

@@ -268,7 +277,7 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of class._System.array");

       } else {

         return new PredefinedDecls(refType, boxType, tickType,

-                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,

+                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, nameFamilyType, datatypeType, dtCtorId,

                                    allocField, classDotArray);

       }

       return null;

@@ -310,8 +319,9 @@ namespace Microsoft.Dafny {
     public Bpl.Program Translate(Program p) {

       Contract.Requires(p != null);

       Contract.Ensures(Contract.Result<Bpl.Program>() != null);

+      

       program = p;

-

+      

       if (sink == null || predef == null) {

         // something went wrong during construction, which reads the prelude; an error has

         // already been printed, so just return an empty program here (which is non-null)

@@ -333,15 +343,18 @@ namespace Microsoft.Dafny {
             // nothing to do--this is treated just like a type parameter

           } else if (d is DatatypeDecl) {

             AddDatatype((DatatypeDecl)d);

+          } else if (d is ModuleDecl) {

+            // submodules have already been added as a top level module, ignore this.

           } else if (d is ClassDecl) {

             AddClassMembers((ClassDecl)d);

-          } else if (d is ModuleDecl) {

-            // nop, sub-modules are handled in their own iteration.

           } else {

             Contract.Assert(false);

           }

         }

       }

+      foreach(var c in fieldConstants.Values) {

+        sink.TopLevelDeclarations.Add(c);

+      }

       return sink;

     }

 

@@ -396,7 +409,7 @@ namespace Microsoft.Dafny {
         if (bvs.Length != 0) {

           q = new Bpl.ExistsExpr(ctor.tok, bvs, q);

         }

-        q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, dId), q);

+        q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, dId), q);

         q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q);

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

 

@@ -525,11 +538,11 @@ namespace Microsoft.Dafny {
       var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType);

       Bpl.Expr cases_body = null;

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId);

+        var disj = FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, cases_dId);

         cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);

       }

       var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-      var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullName, new Bpl.VariableSeq(cases_dBv), cases_resType);

+      var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullCompileName, new Bpl.VariableSeq(cases_dBv), cases_resType);

       cases_fn.Body = cases_body;

       sink.TopLevelDeclarations.Add(cases_fn);

     }

@@ -852,7 +865,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),

           etran.InMethodContext());

       // useViaCanCall: f#canCall(args)

-      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);

 

       // ante := useViaCanCall || (useViaContext && typeAnte && pre)

@@ -957,7 +970,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(0 <= layer && layer < 3);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      string name = f.FullName;

+      string name = f.FullCompileName;

       switch (layer) {

         case 2: name += "#2"; break;

         case 0: name += "#limited"; break;

@@ -1140,7 +1153,7 @@ namespace Microsoft.Dafny {
             foreach (var inFormal in m.Ins) {

               var dt = inFormal.Type.AsDatatype;

               if (dt != null) {

-                var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullName, Bpl.Type.Bool));

+                var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullCompileName, Bpl.Type.Bool));

                 var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));

                 builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));

               }

@@ -1455,8 +1468,8 @@ namespace Microsoft.Dafny {
         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

       }

 

-      string axiomComment = "frame axiom for " + f.FullName;

-      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

+      string axiomComment = "frame axiom for " + f.FullCompileName;

+      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));

       while (fn != null) {

         Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);

         Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

@@ -1578,7 +1591,7 @@ namespace Microsoft.Dafny {
           }

         }

       }

-      Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

+      Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullCompileName, typeParams, inParams, new Bpl.VariableSeq(),

         req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null));

       sink.TopLevelDeclarations.Add(proc);

 

@@ -1640,7 +1653,7 @@ namespace Microsoft.Dafny {
         // don't fall through to postcondition checks

         bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

       } else {

-        Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

+        Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));

         Bpl.ExprSeq args = new Bpl.ExprSeq();

         args.Add(etran.HeapExpr);

         foreach (Variable p in implInParams) {

@@ -1732,7 +1745,7 @@ namespace Microsoft.Dafny {
             t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));

           } else if (e.Field is DatatypeDestructor) {

             var dtor = (DatatypeDestructor)e.Field;

-            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

+            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

           }

           return t;

         }

@@ -1991,7 +2004,7 @@ namespace Microsoft.Dafny {
         // check well-formedness of the other parameters

         r = BplAnd(r, CanCallAssumption(e.Args, etran));

         // get to assume canCall

-        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);

         ExprSeq args = etran.FunctionInvocationArguments(e);

         Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

         r = BplAnd(r, canCallFuncAppl);

@@ -2234,7 +2247,7 @@ namespace Microsoft.Dafny {
           CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);

         } else if (e.Field is DatatypeDestructor) {

           var dtor = (DatatypeDestructor)e.Field;

-          var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

+          var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

           if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {

             // There is only one constructor, so the value must be been constructed by it; might as well assume that here.

             builder.Add(new Bpl.AssumeCmd(expr.tok, correctConstructor));

@@ -2423,7 +2436,7 @@ namespace Microsoft.Dafny {
           }

         }

         // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.

-        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);

         ExprSeq args = etran.FunctionInvocationArguments(e);

         Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

         builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

@@ -2799,12 +2812,26 @@ namespace Microsoft.Dafny {
       if (classes.TryGetValue(cl, out cc)) {

         Contract.Assert(cc != null);

       } else {

-        cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullName, predef.ClassNameType), true);

+        cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), !cl.Module.IsAbstract);

         classes.Add(cl, cc);

       }

       return cc;

     }

 

+    Bpl.Constant GetFieldNameFamily(string n) {

+      Contract.Requires(n != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.Result<Bpl.Constant>() != null);

+      Bpl.Constant cc;

+      if (fieldConstants.TryGetValue(n, out cc)) {

+        Contract.Assert(cc != null);

+      } else {

+        cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, predef.NameFamilyType), true);

+        fieldConstants.Add(n, cc);

+      }

+      return cc;

+    }

+

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

     {

       Contract.Requires(tok != null);

@@ -2864,13 +2891,13 @@ namespace Microsoft.Dafny {
       if (fields.TryGetValue(f, out fc)) {

         Contract.Assert(fc != null);

       } else {

-        // const unique f: Field ty;

+        // const f: Field ty;

         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);

+        fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), false);

         fields.Add(f, fc);

-        // axiom FDim(f) == 0 && DeclType(f) == C;

+        // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f;

         Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0));

-        Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))));

+        Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FieldOfDecl, ty, new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))), new Bpl.IdentifierExpr(f.tok, GetFieldNameFamily(f.Name))), Bpl.Expr.Ident(fc));

         Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType));

         sink.TopLevelDeclarations.Add(ax);

       }

@@ -2897,7 +2924,7 @@ namespace Microsoft.Dafny {
         Bpl.Type receiverType = f.EnclosingClass is ClassDecl ? predef.RefType : predef.DatatypeType;

         args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", receiverType), true));

         Bpl.Formal result = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, ty), false);

-        ff = new Bpl.Function(f.tok, f.FullName, args, result);

+        ff = new Bpl.Function(f.tok, f.FullCompileName, args, result);

         fieldFunctions.Add(f, ff);

         // treat certain fields specially

         if (f.EnclosingClass is ArrayClassDecl) {

@@ -2939,7 +2966,7 @@ namespace Microsoft.Dafny {
         args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true));

       }

       Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);

-      Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);

+      Bpl.Function func = new Bpl.Function(f.tok, f.FullCompileName, typeParams, args, res);

       sink.TopLevelDeclarations.Add(func);

 

       if (f.IsRecursive) {

@@ -2948,7 +2975,7 @@ namespace Microsoft.Dafny {
       }

 

       res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-      Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);

+      Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);

       sink.TopLevelDeclarations.Add(canCallF);

     }

 

@@ -3055,10 +3082,10 @@ namespace Microsoft.Dafny {
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

       string name;

       switch (kind) {

-        case 0: name = "CheckWellformed$$" + m.FullName; break;

-        case 1: name = m.FullName; break;

-        case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;

-        case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;

+        case 0: name = "CheckWellformed$$" + m.FullCompileName; break;

+        case 1: name = m.FullCompileName; break;

+        case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;

+        case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;

         default: Contract.Assert(false); throw new cce.UnreachableException();  // unexpected kind

       }

       Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);

@@ -4435,9 +4462,9 @@ namespace Microsoft.Dafny {
       // Make the call

       string name;

       if (RefinementToken.IsInherited(method.tok, currentModule)) {

-        name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullName);

+        name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);

       } else {

-        name = method.FullName;

+        name = method.FullCompileName;

       }

       Bpl.CallCmd call = new Bpl.CallCmd(tok, name, ins, outs);

       builder.Add(call);

@@ -5307,7 +5334,7 @@ namespace Microsoft.Dafny {
           typeArgs.Add(tRhs.EType);

           rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class._System." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);

         } else if (tRhs.EType is ObjectType) {

-          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken,GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);

+          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken, GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);

         } else {

           rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);

         }

@@ -6541,6 +6568,7 @@ namespace Microsoft.Dafny {
       DtTypeParams, // type parameters of datatype

       TypeTuple,

       DeclType,

+      FieldOfDecl,

       FDim,  // field dimension (0 - named, 1 or more - indexed)

 

       DatatypeCtorId,

@@ -6779,6 +6807,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

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

+        case BuiltinFunction.FieldOfDecl:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation != null);

+          return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok, typeInstantiation) , args);

         case BuiltinFunction.FDim:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

@@ -7022,7 +7054,7 @@ namespace Microsoft.Dafny {
               // Note that "body" does not contain limited calls.

 

               // F#canCall(args)

-              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

               ExprSeq args = etran.FunctionInvocationArguments(fexp);

               Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

 

diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
deleted file mode 100644
index 3d64f8dc..00000000
--- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs
+++ /dev/null
@@ -1,136 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-using System.Diagnostics;

-

-namespace GPUVerify

-{

-    class CrossThreadInvariantProcessor : StandardVisitor

-    {

-        private GPUVerifier verifier;

-        private string procName;

-

-        public CrossThreadInvariantProcessor(GPUVerifier verifier, string procName)

-        {

-            this.verifier = verifier;

-            this.procName = procName;

-        }

-

-        public override Expr VisitNAryExpr(NAryExpr node)

-        {

-            

-            if (node.Fun is FunctionCall)

-            {

-                FunctionCall call = node.Fun as FunctionCall;

-

-                if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))

-                {

-                    return Expr.Eq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),

-                                   new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));

-                }

-

-                if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))

-                {

-                    return Expr.Neq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),

-                                   new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));

-                }

-

-                if (call.Func.Name.Equals("__all"))

-                {

-                    return Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),

-                                   new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));

-                }

-

-                if (call.Func.Name.Equals("__exclusive"))

-                {

-                    return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),

-                                   new VariableDualiser(2, verifier.uniformityAnalyser, procName)

-                                       .VisitExpr(node.Args[0].Clone() as Expr)));

-                }

-

-

-            }

-

-            return base.VisitNAryExpr(node);

-        }

-

-

-        internal EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)

-        {

-            EnsuresSeq result = new EnsuresSeq();

-            foreach (Ensures e in ensuresSeq)

-            {

-                result.Add(new Ensures(e.Free, VisitExpr(e.Condition.Clone() as Expr)));

-            }

-            return result;

-        }

-

-        internal RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)

-        {

-            RequiresSeq result = new RequiresSeq();

-            foreach (Requires r in requiresSeq)

-            {

-                result.Add(new Requires(r.Free, VisitExpr(r.Condition.Clone() as Expr)));

-            }

-            return result;

-        }

-

-        internal void ProcessCrossThreadInvariants(StmtList stmtList)

-        {

-            foreach (BigBlock bb in stmtList.BigBlocks)

-            {

-                ProcessCrossThreadInvariants(bb);

-            }

-        }

-

-        internal void ProcessCrossThreadInvariants(List<Block> blocks)

-        {

-            foreach (Block b in blocks)

-            {

-                b.Cmds = ProcessCrossThreadInvariants(b.Cmds);

-            }

-        }

-

-        private void ProcessCrossThreadInvariants(BigBlock bb)

-        {

-            bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);

-

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd whileCmd = bb.ec as WhileCmd;

-                List<PredicateCmd> newInvariants = new List<PredicateCmd>();

-                foreach (PredicateCmd p in whileCmd.Invariants)

-                {

-                    newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));

-                }

-                whileCmd.Invariants = newInvariants;

-                ProcessCrossThreadInvariants(whileCmd.Body);

-            }

-        }

-

-        private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)

-        {

-            CmdSeq newCommands = new CmdSeq();

-

-            foreach (Cmd c in cmds)

-            {

-                if (c is AssertCmd)

-                {

-                    newCommands.Add(new AssertCmd(c.tok, VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));

-                }

-                else if (c is AssumeCmd)

-                {

-                    newCommands.Add(new AssumeCmd(c.tok, VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));

-                }

-                else

-                {

-                    newCommands.Add(c);

-                }

-            }

-            return newCommands;

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 79a73a29..fdefdebd 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -415,8 +415,6 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_dualised");

             }

 

-            ProcessCrossThreadInvariants();

-

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_cross_thread_invariants");

@@ -621,34 +619,6 @@ namespace GPUVerify
             return result;

         }

 

-        private void ProcessCrossThreadInvariants()

-        {

-            foreach (Declaration d in Program.TopLevelDeclarations)

-            {

-                if (d is Procedure)

-                {

-                    Procedure p = d as Procedure;

-                    p.Requires = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Requires);

-                    p.Ensures = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Ensures);

-                }

-                if (d is Implementation)

-                {

-                    Implementation impl = d as Implementation;

-

-                    if (CommandLineOptions.Unstructured)

-                    {

-                        new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.Blocks);

-                    }

-                    else

-                    {

-                        new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.StructuredStmts);

-                    }

-                }

-

-            }

-        }

-

-

         private void emitProgram(string filename)

         {

             using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl"))

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 0bf1cbc4..9b3b08cb 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -121,7 +121,6 @@
     <Compile Include="LoopInvariantGenerator.cs" />

     <Compile Include="MayBePowerOfTwoAnalyser.cs" />

     <Compile Include="StructuredProgramVisitor.cs" />

-    <Compile Include="CrossThreadInvariantProcessor.cs" />

     <Compile Include="EnabledToPredicateVisitor.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="GPUVerifier.cs" />

@@ -179,4 +178,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index 63720c13..ddaf2062 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -78,11 +78,12 @@ namespace GPUVerify
             {

                 FunctionCall call = node.Fun as FunctionCall;

 

-                if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool") ||

-                    call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool") ||

-                    call.Func.Name.Equals("__all") || call.Func.Name.Equals("__at_most_one"))

+                if (call.Func.Name.Equals("__other_bool") || call.Func.Name.Equals("__other_bv32"))

                 {

-                    return node;

+                    Debug.Assert(id == 1 || id == 2);

+                    int otherId = id == 1 ? 2 : 1;

+                    return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(

+                        node.Args[0]);

                 }

 

             }

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 31afbdfa..8c6ad875 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -425,7 +425,7 @@ namespace Microsoft.Boogie.SMTLib
               xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

             }

             else {

-              labels = CalculatePath(0);

+              labels = CalculatePath(handler.StartingProcId());

               xlabels = labels;

             }

             Model model = GetErrorModel();

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 226b05e7..9df1c086 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -77,7 +77,8 @@ public class BlockPredicator {
         // the first statement in the block.

         var assign = cmdSeq.Last();

         cmdSeq.Truncate(cmdSeq.Length-1);

-        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);

+        Expr newExpr = new EnabledReplacementVisitor(pExpr).VisitExpr(aCmd.Expr);

+        aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(pExpr, newExpr);

         cmdSeq.Add(aCmd);

         // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));

         cmdSeq.Add(assign);

@@ -307,7 +308,26 @@ public class BlockPredicator {
         dwf.InParams = new VariableSeq(

           (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))

             .ToArray());

+

+        if (dwf is Procedure)

+        {

+            var proc = (Procedure)dwf;

+            var newRequires = new RequiresSeq();

+            foreach (Requires r in proc.Requires)

+            {

+                newRequires.Add(new Requires(r.Free,

+                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));

+            }

+            var newEnsures = new EnsuresSeq();

+            foreach (Ensures e in proc.Ensures)

+            {

+                newEnsures.Add(new Ensures(e.Free,

+                    new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));

+            }

+        }

+

       }

+

       try {

         var impl = decl as Implementation;

         if (impl != null)

@@ -326,4 +346,28 @@ public class BlockPredicator {
 

 }

 

+

+class EnabledReplacementVisitor : StandardVisitor

+{

+    private Expr pExpr;

+

+    internal EnabledReplacementVisitor(Expr pExpr)

+    {

+        this.pExpr = pExpr;

+    }

+

+    public override Expr VisitExpr(Expr node)

+    {

+        if (node is IdentifierExpr)

+        {

+            IdentifierExpr iExpr = node as IdentifierExpr;

+            if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))

+            {

+                return pExpr;

+            }

+        }

+        return base.VisitExpr(node);

+    }

+}

+

 }

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e3b1cb2d..1f50d4a8 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -367,6 +367,12 @@ namespace Microsoft.Boogie {
       Undetermined

     }

     public class ErrorHandler {

+      // Used in CheckOutcomeCore

+      public virtual int StartingProcId()

+      {

+          return 0;

+      }

+

       public virtual void OnModel(IList<string> labels, Model model) {

         Contract.Requires(cce.NonNullElements(labels));

       }