internal string Mangle(IFieldReference field) {
      Contract.Requires(field != null);

      field.ResolvedField.Dispatch(this); //compute the hash
      var sb = new StringBuilder();
      sb.Append('_');
      sb.Append((uint)this.hash);
      sb.Append('_');
      this.AppendSanitizedName(sb, field.Name.Value);
      return sb.ToString();
    }

        public ReplacementMethodConstructionContext(IMetadataHost host, IFieldReference originalField, IMethodDefinition fakeMethod, BlockStatement block, bool isAssignment, ILogger log, IReplaceableReference originalReference)
        {
            this.host = host;
            this.block = block;
            this.originalField = originalField;
            this.isAssignment = isAssignment;
            this.log = log;
            this.originalReference = originalReference;

            fakeMethodParameters = fakeMethod.Parameters;
            returnType = fakeMethod.Type;
        }

        public override void Visit(IFieldReference fieldReference)
        {
            if (!alreadySeen.Add(fieldReference))
            {
                return;
            }

            IUnitReference definingUnit = MetadataWriter.GetDefiningUnitReference(fieldReference.GetContainingType(Context), Context);
            if (definingUnit != null && ReferenceEquals(definingUnit, this.module))
            {
                return;
            }

            this.Visit((ITypeMemberReference)fieldReference);
            this.Visit(fieldReference.GetType(Context));
            ReserveFieldToken(fieldReference);
        }

        /// <summary>
        /// Tries to get the first field reference in the method body
        /// </summary>
        /// <param name="body"></param>
        /// <param name="field"></param>
        /// <returns></returns>
        public static bool TryGetFirstFieldReference(IMethodBody body, out IFieldReference field)
        {
            Contract.Requires(body != null);
            Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out field) != null);

            foreach (var operation in body.Operations)
            {
                if (operation.OperationCode == OperationCode.Stfld ||
                    operation.OperationCode == OperationCode.Ldfld)
                {
                    field = (IFieldReference)operation.Value;
                    return field != null;
                }
            }

            field = null;
            return false;
        }

        public override void TraverseChildren(IFieldReference fieldReference)
        {
            log.WriteTrace("Visiting field: {0}.", fieldReference.Name.Value);

            var replaceableField = fieldReference.AsReplaceable(ReplaceableReferenceTypes.FieldAccessor);

            if (registry.IsRegistered(replaceableField))
            {
                var replacementMethodToCall = registry.GetReplacement(replaceableField);

                var replacementExpression = new MethodCall();
                replacementExpression.Type = replacementMethodToCall.Type;
                replacementExpression.Arguments = new List<IExpression>();
                replacementExpression.MethodToCall = replacementMethodToCall;
                replacementExpression.IsStaticCall = true;

                var expressionStatement = parent as ExpressionStatement;
                if (expressionStatement != null)
                {
                    var assignment = expressionStatement.Expression as Assignment;
                    if (assignment != null)
                    {
                        var source = assignment.Source as BoundExpression;
                        if (source != null)
                        {
                            var assignmentSource = source.Definition as FieldReference;
                            if (assignmentSource != null)
                            {
                                if (fieldReference.ResolvedField.Equals(assignmentSource.ResolvedField))
                                {
                                    assignment.Source = replacementExpression;
                                }
                            }
                        }
                    }
                }

                var returnStatement = parent as ReturnStatement;
                if (returnStatement != null)
                {
                    returnStatement.Expression = replacementExpression;
                }
            }
        }

    /// <summary>
    /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
    /// on its type based on the heap representation.
    /// </summary>
    public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
      Bpl.Variable v;
      string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);
      
      fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
      Bpl.IToken tok = field.Token();
      Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);

      if (field.ResolvedField.IsStatic) {
        Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
        v = new Bpl.GlobalVariable(tok, tident);
      }
      else {
        Bpl.Type mt = new Bpl.MapType(tok, new List<Bpl.TypeVariable>(), new List<Bpl.Type>(new Bpl.Type[] {this.RefType}), t);
        Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, mt);
        v = new Bpl.GlobalVariable(tok, tident);
      }
      return v;
    }

        public override void TraverseChildren(IFieldReference fieldReference)
        {
            log.WriteTrace("Visiting field: {0}.", fieldReference.Name.Value);

            var replaceableField = fieldReference.AsReplaceable(ReplaceableReferenceTypes.FieldAssignment);

            if (registry.IsRegistered(replaceableField))
            {
                var replacementMethodToCall = registry.GetReplacement(replaceableField);

                var replacementExpression = new MethodCall();
                replacementExpression.Type = replacementMethodToCall.Type;
                replacementExpression.Arguments = new List<IExpression>();
                replacementExpression.MethodToCall = replacementMethodToCall;
                replacementExpression.IsStaticCall = true;

                var expressionStatement = parent as ExpressionStatement;
                if (expressionStatement != null)
                {
                    var assignment = expressionStatement.Expression as Assignment;
                    if (assignment != null)
                    {
                        var target = assignment.Target.Definition as FieldReference;
                        if (target != null)
                        {
                            // If the target is what we're visiting ...
                            if (target.ResolvedField.Equals(fieldReference.ResolvedField))
                            {
                                if (!fieldReference.ResolvedField.IsStatic)
                                {
                                    replacementExpression.Arguments.Add(assignment.Target.Instance);
                                }

                                replacementExpression.Arguments.Add(assignment.Source);
                                expressionStatement.Expression = replacementExpression;
                            }
                        }
                    }
                }
            }
        }

 /// <summary>
 /// Traverses the unspecialized field reference.
 /// </summary>
 private void TraverseUnspecialized(IFieldReference fieldReference)
 {
     Contract.Requires(fieldReference != null);
       Contract.Requires(!(fieldReference is ISpecializedFieldReference));
       if (!this.objectsThatHaveAlreadyBeenTraversed.Add(fieldReference)) return;
       if (this.preorderVisitor != null) this.preorderVisitor.Visit(fieldReference);
       if (this.stopTraversal) return;
       this.TraverseChildren(fieldReference);
       if (this.stopTraversal) return;
       if (this.postorderVisitor != null) this.postorderVisitor.Visit(fieldReference);
 }

 /// <summary>
 /// Traverses the children of the field reference.
 /// </summary>
 public virtual void TraverseChildren(IFieldReference fieldReference)
 {
     Contract.Requires(fieldReference != null);
       //field reference attributes are distinct from field definition attributes. When a definition serves as a reference, the reference is assumed to be unattributed.
       if (!(fieldReference is IFieldDefinition))
     this.Traverse(fieldReference.Attributes);
       this.Traverse(fieldReference.ContainingType);
       if (this.stopTraversal) return;
       if (fieldReference.IsModified) {
     this.Traverse(fieldReference.CustomModifiers);
     if (this.stopTraversal) return;
       }
       this.Traverse(fieldReference.Type);
 }

 //^ ensures this.path.Count == old(this.path.Count);
 /// <summary>
 /// Performs some computation with the given field reference.
 /// </summary>
 /// <param name="fieldReference"></param>
 public virtual void Visit(IFieldReference fieldReference)
 {
     if (this.stopTraversal) return;
       this.Visit((ITypeMemberReference)fieldReference);
       //^ int oldCount = this.path.Count;
       this.path.Push(fieldReference);
       if (fieldReference.IsModified)
     this.Visit(fieldReference.CustomModifiers);
       //^ assume this.path.Count == oldCount+1; //True because all of the virtual methods of this class promise not decrease this.path.Count.
       this.path.Pop();
 }

        public override void TraverseChildren(IFieldReference fieldReference)
{ MethodEnter(fieldReference);
            base.TraverseChildren(fieldReference);
     MethodExit();   }

    uint GetFieldReferenceInternedId(IFieldReference fieldReference) {
      Contract.Requires(fieldReference != null);

      uint containingTypeReferenceInternedId = this.GetTypeReferenceInternId(fieldReference.ContainingType);
      uint fieldTypeInternedId;
      if (fieldReference.IsModified)
        fieldTypeInternedId = this.GetModifiedTypeReferenceInternId(fieldReference.Type, fieldReference.CustomModifiers);
      else
        fieldTypeInternedId = this.GetTypeReferenceInternId(fieldReference.Type);
      uint fieldNameId = (uint)fieldReference.Name.UniqueKey;
      var fieldsForType = this.FieldReferenceHashtable.Find(containingTypeReferenceInternedId);
      if (fieldsForType == null) {
        fieldsForType = new DoubleHashtable();
        this.FieldReferenceHashtable.Add(containingTypeReferenceInternedId, fieldsForType);
      }
      uint result = fieldsForType.Find(fieldNameId, fieldTypeInternedId);
      if (result == 0) {
        result = this.CurrentFieldReferenceInternValue++;
        fieldsForType.Add(fieldNameId, fieldTypeInternedId, result);
      }
      return result;
    }

 /// <summary>
 /// Performs some computation with the given field reference.
 /// </summary>
 public void Visit(IFieldReference fieldReference)
 {
     this.Visit((ITypeMemberReference)fieldReference);
     if (fieldReference.InternedKey == 0)
       this.ReportError(MetadataError.IncompleteNode, fieldReference, "InternedKey");
     if (fieldReference.Type is Dummy)
       this.ReportError(MetadataError.IncompleteNode, fieldReference, "Type");
     var resolvedField = fieldReference.ResolvedField;
     if (!(resolvedField is Dummy) && fieldReference.InternedKey != resolvedField.InternedKey)
       this.ReportError(MetadataError.FieldReferenceResolvesToDifferentField, fieldReference);
 }

 protected override void ReserveFieldToken(IFieldReference fieldReference)
 {
     this.metadataWriter.GetFieldToken(fieldReference);
 }

 protected override void ReserveFieldToken(IFieldReference fieldReference)
 {
 }

 public static string GetNameWithDeclaringType(IFieldReference value)
 {
     return GetNameWithResolutionScope(value.DeclaringType as ITypeReference) + "." + GetName(value);
 }

    private void ProcessFieldVariable(IFieldReference field, IExpression instance, bool buildSelectExpr) {

      //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField))
      TranslatedExpressions.Push( Bpl.Expr.Ident( 
        this.sink.FindOrCreateFieldVariable(field.ResolvedField) ) );

      this.Visit(instance);

      // if the field access is not a targetexpression we build a select expression
      // otherwise the assignment visitor will build a mapassignment later on
      if (buildSelectExpr) {
        List<Bpl.Expr> elist = new List<Bpl.Expr>();

        while (TranslatedExpressions.Count > 0) {
          elist.Add(TranslatedExpressions.Pop());
        }
        TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(field.Token(), HeapVariable), elist));
      }
    }

 public void Visit(IFieldReference fieldReference)
 {
     throw new NotImplementedException();
 }

 public uint GetFieldInternedKey(IFieldReference fieldReference) {
   return 0;
 }

 public FieldAccessorReplacementBuilder(IFieldReference field, ReplacementRegistry registry)
 {
     this.field = field;
     this.registry = registry;
 }