static string contractRename(Method meth, ArrayList a, ArrayList b)
        {
            MethodContract mc = meth.Contract;

            File.AppendAllText("g:\\test3.txt", meth.HelpText + "\r\n");
            return "";
        }

 private CurrentState(TypeNode type, Dictionary<string, object> typeSuppressed, Method method)
 {
     this.Type = type;
     this.typeSuppressed = typeSuppressed;
     this.Method = method;
     this.methodSuppressed = null;
 }

 public CollectOldExpressions(Module module, Method method, ContractNodes contractNodes, Dictionary<TypeNode, Local> closureLocals, 
     int localCounterStart, Class initialClosureClass)
     : this(module, method, contractNodes, closureLocals, localCounterStart)
 {
     this.topLevelClosureClass = initialClosureClass;
     this.currentClosureClass = initialClosureClass;
 }

 static public void check(TypeSystem t, Method m){
   ModifiesChecker mChecker=new ModifiesChecker(t);
   ControlFlowGraph cfg=ControlFlowGraph.For(m);
   mChecker.Run(cfg,
     null // TBD
     );
 } 

        internal static Block CreateTryFinallyBlock(Method method, Block tryBody, Block finallyBody)
        {
          Contract.Requires(method != null);
          Contract.Requires(tryBody != null);
          Contract.Requires(finallyBody != null);

            if (method.ExceptionHandlers == null) method.ExceptionHandlers = new ExceptionHandlerList();

            Block result = new Block(new StatementList());
            Block afterFinally = new Block(new StatementList());

            tryBody.Statements.Add(new Branch(null, afterFinally, false, true, true));
            finallyBody.Statements.Add(new EndFinally());

            result.Statements.Add(tryBody);
            result.Statements.Add(finallyBody);
            result.Statements.Add(afterFinally);

            ExceptionHandler fb = new ExceptionHandler();
            fb.TryStartBlock = tryBody;
            fb.BlockAfterTryEnd = finallyBody;
            fb.HandlerStartBlock = finallyBody;
            fb.BlockAfterHandlerEnd = afterFinally;
            fb.HandlerType = NodeType.Finally;
            method.ExceptionHandlers.Add(fb);

            return result;
        }

 public CurrentState(AssemblyNode assembly) {
   this.Assembly = assembly;
   this.Type = null;
   this.Method = null;
   this.assemblySuppressed = null;
   this.typeSuppressed = null;
   this.methodSuppressed = null;
 }

 public override Method VisitMethod(Method method)
 {
     if (method == null) return null;
     this.VisitAttributeList(method.Attributes);
     this.VisitAttributeList(method.ReturnAttributes);
     // don't visit further into the method.
     return method;
 }

 public void CheckMethodSpecAdmissibility(Expression exp, Method method, bool reportWFonly, bool dontReport) {
   DeclaringMethod = method;
   ReportWFErrorOnly = reportWFonly; // true for Pure methods: we only want to enforce well-foundedness on them
   DontReportError = dontReport;     
   StateStack = new System.Collections.Stack();
   ResetCurrentState();
   this.VisitExpression(exp);
 }

        public DuplicatorForContractsAndClosures(Module module, Method sourceMethod, Method targetMethod,
            ContractNodes contractNodes, bool mapParameters)
            : base(module, targetMethod.DeclaringType)
        {
            this.sourceMethod = sourceMethod;
            this.targetMethod = targetMethod;

            this.RemoveNameForLocals = true;

            Duplicator dup = this;

            if (mapParameters)
            {
                if (sourceMethod.ThisParameter != null)
                {
                    if (targetMethod.ThisParameter != null)
                    {
                        dup.DuplicateFor[sourceMethod.ThisParameter.UniqueKey] = targetMethod.ThisParameter;
                    }
                    else
                    {
                        // target is a static wrapper. But duplicator cannot handle This -> Parameter conversion
                        // so we handle it explicitly here in this visitor.
                        replaceThisWithParameter = targetMethod.Parameters[0];
                    }
                }

                if (sourceMethod.Parameters != null && targetMethod.Parameters != null
                    && sourceMethod.Parameters.Count == targetMethod.Parameters.Count)
                {
                    for (int i = 0, n = sourceMethod.Parameters.Count; i < n; i++)
                    {
                        dup.DuplicateFor[sourceMethod.Parameters[i].UniqueKey] = targetMethod.Parameters[i];
                    }
                }
            }

            var originalType = HelperMethods.IsContractTypeForSomeOtherType(sourceMethod.DeclaringType, contractNodes);
            if (originalType != null)
            {
                var contractType = this.contractClass = sourceMethod.DeclaringType;
                while (contractType.Template != null)
                {
                    contractType = contractType.Template;
                }
                    
                while (originalType.Template != null)
                {
                    originalType = originalType.Template;
                }

                // forward ContractType<A,B> -> originalType<A',B'>
                this.contractClassToForward = contractType;
                this.targetTypeToForwardTo = originalType;

                //dup.DuplicateFor[contractType.UniqueKey] = originalType;
            }
        }

        public override Method VisitMethod(Method method)
        {
            if (method == null) return null;

            ZMethod result = (ZMethod)base.VisitMethod(method);

            result.ResetLocals();
            return result;
        }

 public CurrentState(TypeNode type, CurrentState oldState)
 {
     this.Type = type;
     this.Method = null;
     this.typeSuppressed = null;
     this.methodSuppressed = null;
     this.Assembly = oldState.Assembly;
     this.assemblySuppressed = oldState.assemblySuppressed;
 }

 /// <summary>
 /// Visits the ensures clauses to clean up Old expressions
 /// </summary>
 /// <param name="m"></param>
 public void CleanupEnsures(Method m)
 {
     if (m.Contract != null)
     {
         this.VisitEnsuresList(m.Contract.Ensures);
         this.VisitEnsuresList(m.Contract.AsyncEnsures);
         this.VisitEnsuresList(m.Contract.ModelEnsures);
     }
 }

        /// <summary>
        /// actualReturn type is null if Task is not generic, otherwise ,the Task result type.
        /// </summary>
        public static bool Contains(Node node, ContractNodes contractNodes, Method currentMethod,
            TypeNode actualReturnType)
        {
            var v = new AsyncReturnValueQuery(contractNodes, currentMethod, actualReturnType);

            v.Visit(node);

            return v.foundReturnValueTaskResult;
        }

        // Requires:
        //  statement.Expression is MethodCall
        //  statement.Expression.Callee is MemberBinding
        //  statement.Expression.Callee.BoundMember is Method
        //  statement.Expression.Callee.BoundMember == "Requires" or "Ensures"
        //
        //  inline  <==> replacementMethod == null
        //  replacementMethod != null
        //           ==> replacementMethod.ReturnType == methodToReplace.ReturnType
        //               && replacementMethod.Parameters.Count == 1
        //               && methodToReplace.Parameters.Count == 1
        //               && replacementMethod.Parameters[0].Type == methodToReplace.Parameters[0].Type
        //
        private static Statement RewriteContractCall(
            ExpressionStatement statement,
            Method /*!*/ methodToReplace,
            Method /*?*/ replacementMethod,
            Literal /*?*/ sourceTextToUseAsSecondArg)
        {
            Contract.Requires(statement != null);

            MethodCall call = statement.Expression as MethodCall;

            if (call == null || call.Callee == null)
            {
                return statement;
            }

            MemberBinding mb = call.Callee as MemberBinding;
            if (mb == null)
            {
                return statement;
            }

            Method m = mb.BoundMember as Method;
            if (m == null)
            {
                return statement;
            }

            if (m != methodToReplace)
            {
                return statement;
            }

            mb.BoundMember = replacementMethod;

            if (call.Operands.Count == 3)
            {
                // then the invariant was found in a reference assembly
                // it already has all of its arguments
                return statement;
            }

            if (call.Operands.Count == 1)
            {
                call.Operands.Add(Literal.Null);
            }

            Literal extraArg = sourceTextToUseAsSecondArg;
            if (extraArg == null)
            {
                extraArg = Literal.Null;
                //extraArg = new Literal("No other information available", SystemTypes.String);
            }

            call.Operands.Add(extraArg);

            return statement;
        }

        public override Method VisitMethod(Method method)
        {
            Method re = base.VisitMethod(method);

            System.Compiler.TypeNode sigTmp = re.ReturnType;
            if(sigTmp.TypeCode!=TypeCode.Empty)
                signatureType = sigTmp;

            return re;
        }

        /// <summary>
        /// 
        /// </summary>
        /// <param name="writer"></param>
        /// <param name="type">the current type being extended</param>
        /// <param name="extensionMethodTemplate">A reference to the extension method. For generic methods, this is a reference to the 
        /// non-specialized method, e.g. System.Linq.Enumerable.Select``2.
        /// </param>
        /// <param name="specialization">When the current type implements or inherits from a specialization of a generic type,
        /// this parameter has a TypeNode for the type used as apecialization of the generic type's first template param. 
        /// </param>
        private void AddExtensionMethod(XmlWriter writer, TypeNode type, Method extensionMethodTemplate, TypeNode specialization)
        {
            // If this is a specialization of a generic method, construct a Method object that describes the specialization
            Method extensionMethodTemplate2 = extensionMethodTemplate;
            if (extensionMethodTemplate2.IsGeneric && (specialization != null))
            {
                // the specialization type is the first of the method's template arguments
                TypeNodeList templateArgs = new TypeNodeList();
                templateArgs.Add(specialization);
                // add any additional template arguments
                for (int i = 1; i < extensionMethodTemplate.TemplateParameters.Count; i++)
                    templateArgs.Add(extensionMethodTemplate.TemplateParameters[i]);
                extensionMethodTemplate2 = extensionMethodTemplate.GetTemplateInstance(type, templateArgs);
            }
            TypeNode extensionMethodTemplateReturnType = extensionMethodTemplate2.ReturnType;
            ParameterList extensionMethodTemplateParameters = extensionMethodTemplate2.Parameters;

            ParameterList extensionMethodParameters = new ParameterList();
            for (int i = 1; i < extensionMethodTemplateParameters.Count; i++)
            {
                Parameter extensionMethodParameter = extensionMethodTemplateParameters[i];
                extensionMethodParameters.Add(extensionMethodParameter);
            }
            Method extensionMethod = new Method(extensionMethodTemplate.DeclaringType, new AttributeList(), extensionMethodTemplate.Name, extensionMethodParameters, extensionMethodTemplate.ReturnType, null);
            extensionMethod.Flags = extensionMethodTemplate.Flags & ~MethodFlags.Static;

            // for generic methods, set the template args and params so the template data is included in the id and the method data
            if (extensionMethodTemplate2.IsGeneric)
            {
                extensionMethod.IsGeneric = true;
                if (specialization != null)
                {
                    // set the template args for the specialized generic method
                    extensionMethod.TemplateArguments = extensionMethodTemplate2.TemplateArguments;
                }
                else
                {
                    // set the generic template params for the non-specialized generic method
                    extensionMethod.TemplateParameters = extensionMethodTemplate2.TemplateParameters;
                }
            }

            // Get the id
            string extensionMethodTemplateId = reflector.ApiNamer.GetMemberName(extensionMethodTemplate);

            // write the element node
            writer.WriteStartElement("element");
            writer.WriteAttributeString("api", extensionMethodTemplateId);
            writer.WriteAttributeString("source", "extension");
            isExtensionMethod = true;
            reflector.WriteMember(extensionMethod);
            isExtensionMethod = false;
            writer.WriteEndElement();
        }

 private CodeFlattener(Method method, bool expandAllocations, bool constantFold) 
 {
   this.Method = method;
   this.expandAllocations = expandAllocations;
   this.performConstantFoldingOnBranchConditions = constantFold;
   this.new_stats = new StatementList();
   this.new_blocks = new StatementList();
   this.thisNode = CciHelper.GetThis(method);
   if (thisNode != null && thisNode.Type == null) {
     thisNode.Type = method.DeclaringType;
   }
 }

        public AbbreviationDuplicator(Method sourceMethod, Method targetMethod, ContractNodes contractNodes,
            Method abbreviation, Expression targetObject, ExpressionList actuals)
            : base(targetMethod.DeclaringType.DeclaringModule, sourceMethod, targetMethod, contractNodes, false)
        {
            this.targetObject = targetObject;
            this.abbreviation = abbreviation;
            this.actuals = actuals;

            this.localsInActuals = new TrivialHashtable();

            PopulateLocalsInActuals();
        }

 public override void VisitMethod(Method method)
 {
     if (method == null) return;
     var savedCurrentMethod = this.CurrentMethod;
     this.CurrentMethod = method;
     try
     {
         base.VisitMethod(method);
     }
     finally
     {
         this.CurrentMethod = savedCurrentMethod;
     }
 }

        protected override void LanguageSpecificAnalysis(Method method)
        {
            if (!this.CodeIsWellFormed)
                return;
            if (Cci.Analyzer.Debug)
            {
                ControlFlowGraph cfg = GetCFG(method);
                if (cfg != null) cfg.Display(Console.Out);
            }
            if (method.Name.Name.StartsWith("Microsoft.Contracts"))
                return;
            // Weak Purity and Effects Analysis
            if (this.WeakPurityAnalysis && this.WeakPurityAnalyzer != null)
            {
                this.WeakPurityAnalyzer.VisitMethod(method); // computes points-to and effects
                // processes results from VisitMethod: issues errors and potentially prints out detailed info.
                this.WeakPurityAnalyzer.ProcessResultsMethod(method);

                // Admissibility Check 
                PointsToAndWriteEffects ptwe = this.WeakPurityAnalyzer.GetPurityAnalysisWithDefault(method);
                if (method.IsConfined || method.IsStateIndependent)
                {
                    Microsoft.SpecSharp.ReadEffectAdmissibilityChecker reac = new Microsoft.SpecSharp.ReadEffectAdmissibilityChecker(method, typeSystem.ErrorHandler);
                    reac.CheckReadEffectAdmissibility(ptwe.ComputeEffects(ptwe.ReadEffects));
                }

            }

            if (ReentrancyAnalysis)
            {
                if (this.ReentrancyAnalyzer != null)
                {
                    this.ReentrancyAnalyzer.VisitMethod(method);
                }
            }

            if (ObjectExposureAnalysis)
            {
                if (this.ObjectExposureAnalyzer != null)
                {
                    this.ObjectExposureAnalyzer.VisitMethod(method);
                }
            }
        }