/// <summary>
 /// Return zero or more locations in primary source documents that correspond to the definition of the given local.
 /// </summary>
 public IEnumerable<IPrimarySourceLocation> GetPrimarySourceLocationsForDefinitionOf(ILocalDefinition localDefinition) {
   ISourceLocationProvider/*?*/ provider = this.GetProvider(localDefinition);
   if (provider == null)
     return Enumerable<IPrimarySourceLocation>.Empty;
   else
     return provider.GetPrimarySourceLocationsForDefinitionOf(localDefinition);
 }

 public override void Visit(ILocalDefinition localDefinition)
 {
     NewLineAddIndent();
     AppendElementType(localDefinition);
     //output.Append(localDefinition.Name.Value);
     //AppendSpace();
     base.Visit(localDefinition);
 }

 /// <summary>
 /// Returns the source name of the given local definition, if this is available.
 /// Otherwise returns the value of the Name property and sets isCompilerGenerated to true.
 /// </summary>
 public string GetSourceNameFor(ILocalDefinition localDefinition, out bool isCompilerGenerated) {
   ISourceLocationProvider/*?*/ provider = this.GetProvider(localDefinition);
   if (provider == null) {
     isCompilerGenerated = false;
     return "";
   } else {
     return provider.GetSourceNameFor(localDefinition, out isCompilerGenerated);
   }
 }

 /// <summary>
 /// 
 /// </summary>
 /// <param name="local"></param>
 /// <returns></returns>
 public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {
   Bpl.LocalVariable v;
   Bpl.IToken tok = local.Token();
   Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);
   if (!localVarMap.TryGetValue(local, out v)) {
     v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
     localVarMap.Add(local, v);
   }
   return v;
 }

 /// <summary>
 /// Visits the specified local definition.
 /// </summary>
 /// <param name="localDefinition">The local definition.</param>
 public virtual void Visit(ILocalDefinition localDefinition)
 {
     if (this.stopTraversal) return;
       //^ int oldCount = this.path.Count;
       this.path.Push(localDefinition);
       if (localDefinition.IsModified)
     this.Visit(localDefinition.CustomModifiers);
       this.Visit(localDefinition.Type);
       //^ assume this.path.Count == oldCount+1; //True because all of the virtual methods of this class promise not to decrease this.path.Count.
       this.path.Pop();
 }

 public virtual void Visit(ILocalDefinition localDefinition)
 {
     this.Visit(localDefinition.CustomModifiers);
     this.Visit(localDefinition.Type);
 }

 private ILocalDefinition GetLocalWithSourceName(ILocalDefinition localDef) {
   Contract.Requires(localDef != null);
   Contract.Ensures(Contract.Result<ILocalDefinition>() != null);
   return this.sourceMethodBody.GetLocalWithSourceName(localDef);
 }

 /*?*/
 private ILocalScopeProvider GetProvider(ILocalDefinition localDefinition)
 {
     return this.GetProvider(localDefinition.MethodDefinition);
 }

 public override void TraverseChildren(ILocalDefinition localDefinition)
 {
     if (!foundLocals.Contains(localDefinition)) foundLocals.Add(localDefinition);
     base.TraverseChildren(localDefinition);
 }

 /// <summary>
 /// Performs some computation with the given local definition.
 /// </summary>
 public void VisitReference(ILocalDefinition localDefinition)
 {
 }

 private ILocalDefinition GetLocalWithSourceName(ILocalDefinition localDef)
 {
     if (this.sourceLocationProvider == null) return localDef;
       var mutableLocal = this.localMap[localDef];
       if (mutableLocal != null) return mutableLocal;
       mutableLocal = localDef as LocalDefinition;
       if (mutableLocal == null) {
     mutableLocal = new LocalDefinition();
     mutableLocal.Copy(localDef, this.host.InternFactory);
       }
       this.localMap.Add(localDef, mutableLocal);
       bool isCompilerGenerated;
       var sourceName = this.sourceLocationProvider.GetSourceNameFor(localDef, out isCompilerGenerated);
       if (sourceName != localDef.Name.Value) {
     mutableLocal.Name = this.host.NameTable.GetNameFor(sourceName);
       }
       return mutableLocal;
 }

 private static IEnumerable<string> GetTypesOfVariable(ILocalDefinition variable)
 {
     return from t in variable.Type.GetAllRealTypeReferences()
            select t.ToString();
 }

 /// <summary>
 /// Traverses the children of the specified local definition.
 /// </summary>
 public virtual void TraverseChildren(ILocalDefinition localDefinition)
 {
     Contract.Requires(localDefinition != null);
       if (localDefinition.IsConstant)
     this.Traverse(localDefinition.CompileTimeValue);
       if (localDefinition.IsModified)
     this.Traverse(localDefinition.CustomModifiers);
       if (this.stopTraversal) return;
       this.Traverse(localDefinition.Type);
 }

 /// <summary>
 /// Traverses the specified local definition.
 /// </summary>
 public void Traverse(ILocalDefinition localDefinition)
 {
     Contract.Requires(localDefinition != null);
       if (!this.objectsThatHaveAlreadyBeenTraversed.Add(localDefinition)) return;
       if (this.preorderVisitor != null) this.preorderVisitor.Visit(localDefinition);
       if (this.stopTraversal) return;
       this.TraverseChildren(localDefinition);
       if (this.stopTraversal) return;
       if (this.postorderVisitor != null) this.postorderVisitor.Visit(localDefinition);
 }

 private PdbFunction GetPdbFunctionFor(ILocalDefinition localDefinition)
 {
     PdbFunction/*?*/ result = null;
       foreach (ILocation location in localDefinition.Locations) {
     MethodBodyLocation/*?*/ mbLocation = location as MethodBodyLocation;
     if (mbLocation != null) {
       this.pdbFunctionMap.TryGetValue(mbLocation.Document.MethodToken, out result);
       break;
     }
       }
       return result;
 }

 /// <summary>
 /// 
 /// </summary>
 /// <param name="localDefinition"></param>
 /// <param name="isCompilerGenerated"></param>
 /// <returns></returns>
 public string GetSourceNameFor(ILocalDefinition localDefinition, out bool isCompilerGenerated)
 {
     isCompilerGenerated = true;
       PdbFunction/*?*/ pdbFunction = this.GetPdbFunctionFor(localDefinition);
       if (pdbFunction != null) {
     uint index = 0;
     foreach (ILocation location in localDefinition.Locations) {
       MethodBodyLocation/*?*/ mbLocation = location as MethodBodyLocation;
       if (mbLocation != null) {
     index = mbLocation.Offset;
     break;
       }
     }
     PdbSlot/*?*/ slot = this.GetSlotFor(pdbFunction.scopes, index);
     if (slot != null) {
       isCompilerGenerated = (slot.flags & 0x4) != 0;
       return slot.name;
     }
       }
       return localDefinition.Name.Value;
 }

 /// <summary>
 /// Return zero or more locations in primary source documents that correspond to the definition of the given local.
 /// </summary>
 public IEnumerable<IPrimarySourceLocation> GetPrimarySourceLocationsForDefinitionOf(ILocalDefinition localDefinition)
 {
     PdbFunction/*?*/ pdbFunction = this.GetPdbFunctionFor(localDefinition);
       if (pdbFunction != null) {
     uint index = 0;
     foreach (ILocation location in localDefinition.Locations) {
       MethodBodyLocation/*?*/ mbLocation = location as MethodBodyLocation;
       if (mbLocation != null) {
     index = mbLocation.Offset;
     break;
       }
     }
     PdbSlot/*?*/ slot = this.GetSlotFor(pdbFunction.scopes, index);
     if (slot != null && (slot.flags & 0x4) == 0)
       return IteratorHelper.GetSingletonEnumerable<IPrimarySourceLocation>(new LocalNameSourceLocation(slot.name));
       }
       return IteratorHelper.GetEmptyEnumerable<IPrimarySourceLocation>();
 }

 public void VisitReference(ILocalDefinition localDefinition)
 {
     Contract.Assume(false);
 }

 /// <summary>
 /// Performs some computation with the given local definition.
 /// </summary>
 public void Visit(ILocalDefinition localDefinition)
 {
 }

 public virtual void PrintLocalName(ILocalDefinition local) {
   this.sourceEmitterOutput.Write(local.Name.Value);
 }