public ExtractorVisitor(ContractNodes /*!*/ contractNodes,
            AssemblyNode ultimateTargetAssembly,
            AssemblyNode realAssembly,
            bool verbose,
            bool fSharp)
        {
            Contract.Requires(contractNodes != null);
            Contract.Requires(realAssembly != null);

            this.contractNodes = contractNodes;
            this.verbose = verbose;
            this.fSharp = fSharp;
            this.visibility = new VisibilityHelper();
            this.errorFound = false;
            this.extractionFinalizer = new ExtractionFinalizer(contractNodes);
            this.ultimateTargetAssembly = ultimateTargetAssembly;
            this.realAssembly = realAssembly;

            this.contractNodes.ErrorFound += delegate(CompilerError error)
            {
                // Commented out because the ErrorFound event already had a handler that was printing out a message
                // and so error messages were getting printed out twice
                //if (!error.IsWarning || warningLevel > 0) {
                //  Console.WriteLine(error.ToString());
                //}
                errorFound |= !error.IsWarning;
            };

            this.TaskType = new Cache<TypeNode>(() => HelperMethods.FindType(realAssembly, Identifier.For("System.Threading.Tasks"), Identifier.For("Task")));

            this.GenericTaskType = new Cache<TypeNode>(() =>
                HelperMethods.FindType(realAssembly, Identifier.For("System.Threading.Tasks"),
                    Identifier.For("Task" + TargetPlatform.GenericTypeNamesMangleChar + "1")));
        }

 public ClousotExtractor(ContractNodes contractNodes, AssemblyNode ultimateTargetAssembly,
     AssemblyNode realAssembly, Action<System.CodeDom.Compiler.CompilerError> errorHandler)
     : base(contractNodes, ultimateTargetAssembly, realAssembly)
 {
     Contract.Requires(contractNodes != null);
     Contract.Requires(realAssembly != null);
 }

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

        public static Method FindShadow(this Method method, AssemblyNode shadowAssembly)
        {
            var shadowParent = method.DeclaringType.FindShadow(shadowAssembly);

            if (shadowParent == null) return null;

            return shadowParent.FindShadow(method);
        }

 public virtual void Add(AssemblyNode assembly) {
     if (assembly == null) throw new ArgumentNullException("assembly");
     string name = assembly.StrongName;
     assembly.AssemblyReferenceResolution += new Module.AssemblyReferenceResolver(ResolveReference);
     assembly.AssemblyReferenceResolutionAfterProbingFailed += new Module.AssemblyReferenceResolver(UnresolvedReference);
     cache[name] = assembly;
     //Console.WriteLine("added {0}; cache now contains {1}", name, cache.Count);
 }

 internal TypeNode GetTypeNodeFor(AssemblyNode assembly, Type t) {
   if (t.IsArray) {
     int rank = t.GetArrayRank();
     Type et = t.GetElementType();
     TypeNode type = assembly.GetType(Identifier.For(et.Namespace), Identifier.For(et.Name));
     return type.GetArrayType(rank);
   } else {        
     return assembly.GetType(Identifier.For(t.Namespace), Identifier.For(t.Name));
   }    
 }

        public CopyOutOfBandContracts(AssemblyNode targetAssembly, AssemblyNode sourceAssembly,
            ContractNodes contractNodes, ContractNodes targetContractNodes)
        {
            Contract.Requires(targetAssembly != null);
            Contract.Requires(sourceAssembly != null);
            Contract.Requires(contractNodes != null);

            if (targetAssembly == sourceAssembly)
            {
                // this happened when a reference assembly for mscorlib had the assembly name "mscorlib"
                // instead of "mscorlib.Contracts" because only one assembly named "mscorlib" can be
                // loaded
                throw new ExtractorException("CopyOutOfBandContracts was given the same assembly as both the source and target!");
            }

            this.outOfBandDuplicator = new ForwardingDuplicator(targetAssembly, null, contractNodes, targetContractNodes);
            this.targetAssembly = targetAssembly;

            FuzzilyForwardReferencesFromSource2Target(targetAssembly, sourceAssembly);

            CopyMissingMembers();

            // FixupMissingProperties(); shouldn't be needed with new duplicator
        }

        private bool SkipThisTypeDueToMismatchInReferenceAssemblyPlatform(AssemblyNode ultimateTargetAssembly,
            TypeNode typeNode)
        {
            if (ultimateTargetAssembly == null) return false;

            if (typeNode == this.contractNodes.ContractClass)
                return false; // don't skip contract methods as we need to extract their contracts

            if (HelperMethods.IsCompilerGenerated(typeNode)) return false; // don't skip closures etc.
            var typeWithSeparateContractClass = HelperMethods.IsContractTypeForSomeOtherTypeUnspecialized(typeNode, this.contractNodes);

            if (typeWithSeparateContractClass != null)
            {
                typeNode = typeWithSeparateContractClass; // see if this one is skipped
            }

            // now see if we have corresponding target type
            if (typeNode.FindShadow(ultimateTargetAssembly) != null) return false; // have target

            return true; // skip it.
        }

        private static TypeNode GetPossiblyNestedType(AssemblyNode assem, string namespaceName, string className)
        {
            Contract.Requires(assem != null);
            Contract.Requires(className != null);

            var ns = Identifier.For(namespaceName);

            string[] pieces = className.Split('.');

            // Get outermost type
            string outerMost = pieces[0];
            TypeNode t = assem.GetType(ns, Identifier.For(outerMost));

            if (t == null) return null;

            for (int i = 1; i < pieces.Length; i++)
            {
                var piece = pieces[i];
                t = t.GetNestedType(Identifier.For(piece));
                
                if (t == null) return null;
            }

            return t;
        }

 public void VisitForPostCheck(AssemblyNode assemblyNode)
 {
     this.VisitAssembly(assemblyNode);
 }

 private AssemblyNode ReadAssembly(AssemblyNode.PostAssemblyLoadProcessor postLoadEvent){

        private static ContractNodes IdentifyContractAssemblyIfReferenced(ContractNodes contracts, AssemblyNode assemblyToVisit)
        {
            Contract.Requires(assemblyToVisit != null);

            if (contracts != null)
            {
                AssemblyNode assemblyContractsLiveIn = contracts.ContractClass == null
                    ? null
                    : contracts.ContractClass.DeclaringModule as AssemblyNode;

                if (assemblyContractsLiveIn != null)
                {
                    if (assemblyContractsLiveIn == assemblyToVisit)
                    {
                        return contracts;
                    }
                    
                    string nameOfAssemblyContainingContracts = assemblyContractsLiveIn.Name;
                    
                    Contract.Assume(assemblyToVisit.AssemblyReferences != null);
                    
                    foreach (var ar in assemblyToVisit.AssemblyReferences)
                    {
                        Contract.Assume(ar != null);

                        if (ar.Name == nameOfAssemblyContainingContracts)
                        {
                            // just do name matching to avoid loading the referenced assembly
                            return contracts;
                        }
                    }
                }
            }

            return null;
        }

    /// <summary>
    /// Tries to reuse or create the attribute
    /// </summary>
    private static InstanceInitializer GetRuntimeContractsAttributeCtor(AssemblyNode assembly)
    {
      EnumNode runtimeContractsFlags = assembly.GetType(ContractNodes.ContractNamespace, Identifier.For("RuntimeContractsFlags")) as EnumNode;
      Class RuntimeContractsAttributeClass = assembly.GetType(ContractNodes.ContractNamespace, Identifier.For("RuntimeContractsAttribute")) as Class;

      if (runtimeContractsFlags == null)
      {
        #region Add [Flags]
        Member flagsConstructor = RewriteHelper.flagsAttributeNode.GetConstructor();
        AttributeNode flagsAttribute = new AttributeNode(new MemberBinding(null, flagsConstructor), null, AttributeTargets.Class);
        #endregion Add [Flags]
        runtimeContractsFlags = new EnumNode(assembly,
          null, /* declaringType */
          new AttributeList(2),
          TypeFlags.Sealed,
          ContractNodes.ContractNamespace,
          Identifier.For("RuntimeContractsFlags"),
          new InterfaceList(),
          new MemberList());
        runtimeContractsFlags.Attributes.Add(flagsAttribute);
        RewriteHelper.TryAddCompilerGeneratedAttribute(runtimeContractsFlags);
        runtimeContractsFlags.UnderlyingType = SystemTypes.Int32;

        Type copyFrom = typeof(RuntimeContractEmitFlags);
        foreach (System.Reflection.FieldInfo fi in copyFrom.GetFields())
        {
          if (fi.IsLiteral)
          {
            AddEnumValue(runtimeContractsFlags, fi.Name, fi.GetRawConstantValue());
          }
        }
        assembly.Types.Add(runtimeContractsFlags);

      }


      InstanceInitializer ctor = (RuntimeContractsAttributeClass == null) ? null : RuntimeContractsAttributeClass.GetConstructor(runtimeContractsFlags);

      if (RuntimeContractsAttributeClass == null)
      {
        RuntimeContractsAttributeClass = new Class(assembly,
          null, /* declaringType */
          new AttributeList(),
          TypeFlags.Sealed,
          ContractNodes.ContractNamespace,
          Identifier.For("RuntimeContractsAttribute"),
          SystemTypes.Attribute,
          new InterfaceList(),
          new MemberList(0));

        RewriteHelper.TryAddCompilerGeneratedAttribute(RuntimeContractsAttributeClass);
        assembly.Types.Add(RuntimeContractsAttributeClass);
      }
      if (ctor == null) {

        Block returnBlock = new Block(new StatementList(new Return()));

        Block body = new Block(new StatementList());
        Block b = new Block(new StatementList());
        ParameterList pl = new ParameterList();
        Parameter levelParameter = new Parameter(Identifier.For("contractFlags"), runtimeContractsFlags);
        pl.Add(levelParameter);

        ctor = new InstanceInitializer(RuntimeContractsAttributeClass, null, pl, body);
        ctor.Flags = MethodFlags.Assembly | MethodFlags.HideBySig | MethodFlags.SpecialName | MethodFlags.RTSpecialName;

        Method baseCtor = SystemTypes.Attribute.GetConstructor();

        b.Statements.Add(new ExpressionStatement(new MethodCall(new MemberBinding(null, baseCtor), new ExpressionList(ctor.ThisParameter))));
        b.Statements.Add(returnBlock);
        body.Statements.Add(b);

        RuntimeContractsAttributeClass.Members.Add(ctor);
      }

      return ctor;
    }

    /// <summary>
    /// Adds a flag to an assembly that designates it as having runtime contract checks.
    /// Does this by defining the type of the attribute and then marking the assembly with
    /// and instance of that attribute.
    /// </summary>
    /// <param name="assembly">Assembly to flag.</param>
    private void SetRuntimeContractFlag(AssemblyNode assembly) {

      InstanceInitializer ctor = GetRuntimeContractsAttributeCtor(assembly);
      ExpressionList args = new ExpressionList();
      args.Add(new Literal(this.contractEmitFlags, ctor.Parameters[0].Type));
      AttributeNode attribute = new AttributeNode(new MemberBinding(null, ctor), args, AttributeTargets.Assembly);
      assembly.Attributes.Add(attribute);
    }

    public override void VisitAssembly(AssemblyNode assembly)
    {
      // Don't rewrite assemblies twice.
      if (ContractNodes.IsAlreadyRewritten(assembly)) {
        throw new RewriteException("Cannot rewrite an assembly that has already been rewritten!");
      }

      this.module = assembly;

      this.AdaptRuntimeOptionsBasedOnAttributes(assembly.Attributes);

      // Extract all inline foxtrot contracts and place them in the object model.
      //if (this.extractContracts) {
      //  new Extractor(rewriterNodes, this.Verbose, this.Decompile).Visit(assembly);
      //}
      base.VisitAssembly(assembly);

      this.runtimeContracts.Commit();

      // Set the flag that indicates the assembly has been rewritten.
      SetRuntimeContractFlag(assembly);

      // Add wrapper types for call-site requires. We do it here to avoid visiting them multiple times
      foreach (TypeNode t in this.wrapperTypes.Values)
      {
        assembly.Types.Add(t);
      }

      // in principle we shouldn't have old and result left over, but because of the call-site requires copying
      // we end up having them in closures that were used in ensures but not needed at call site requires
#if !DEBUG || true
      CleanUpOldAndResult cuoar = new CleanUpOldAndResult();
      assembly = cuoar.VisitAssembly(assembly);
#endif
      RemoveContractClasses rcc = new RemoveContractClasses();
      rcc.VisitAssembly(assembly);
    }

    /// <summary>
    /// For level, see TranslateLevel
    /// </summary>
    /// <param name="assemblyBeingRewritten"></param>
    /// <param name="rewriterNodes"></param>
    /// <param name="level"></param>
    public Rewriter(AssemblyNode assemblyBeingRewritten, RuntimeContractMethods runtimeContracts, Action<System.CodeDom.Compiler.CompilerError> handleError, bool inheritInvariantsAcrossAssemblies, bool skipQuantifiers)
    {
      Contract.Requires(handleError != null);

      // F:
      Contract.Requires(runtimeContracts != null);

      #region Find IDisposable.Dispose method
      TypeNode iDisposable = SystemTypes.IDisposable;
      if (iDisposable != null)
      {
        IDisposeMethod = iDisposable.GetMethod(Identifier.For("Dispose"));
      }
      #endregion

      this.runtimeContracts = runtimeContracts;
      this.assemblyBeingRewritten = assemblyBeingRewritten;
      this.rewriterNodes = runtimeContracts.ContractNodes;

      this.contractEmitFlags = TranslateLevel(this.runtimeContracts.RewriteLevel);

      this.contractEmitFlags |= RuntimeContractEmitFlags.InheritContracts; // default

      if (runtimeContracts.ThrowOnFailure)
      {
        this.contractEmitFlags |= RuntimeContractEmitFlags.ThrowOnFailure;
      }
      if (!runtimeContracts.UseExplicitValidation)
      {
        this.contractEmitFlags |= RuntimeContractEmitFlags.StandardMode;
      }
      this.m_handleError = handleError;
      this.InheritInvariantsAcrossAssemblies = inheritInvariantsAcrossAssemblies;
      this.skipQuantifiers = skipQuantifiers;
    }

    public RuntimeContractMethods(TypeNode userContractType, ContractNodes contractNodes, AssemblyNode targetAssembly,
                                  bool throwOnFailure, int rewriteLevel, bool publicSurfaceOnly, bool callSiteRequires,
                                  int recursionGuard, bool hideFromDebugger,
                                  bool userExplicitValidation
                                 )
    {
      this.contractNodes = contractNodes;
      this.targetAssembly = targetAssembly;
      this.ThrowOnFailure = throwOnFailure;
      this.RewriteLevel = rewriteLevel;
      this.PublicSurfaceOnly = publicSurfaceOnly;
      this.CallSiteRequires = callSiteRequires;
      this.regularRecursionGuard = recursionGuard;
      this.HideFromDebugger = hideFromDebugger;
      this.UseExplicitValidation = userExplicitValidation;

      // extract methods from user methods
      #region Get the user-specified rewriter methods (optional) REVIEW!! Needs a lot of error handling
      if (userContractType != null)
      {
        Method method = null;
        MethodList reqMethods = userContractType.GetMethods(Identifier.For("Requires"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String);
        for (int i = 0; i < reqMethods.Count; i++)
        {
          method = reqMethods[i];
          if (method != null)
          {
            if (method.TemplateParameters == null || method.TemplateParameters.Count != 1)
            {
              /*if (method != null) */ this.requiresMethod = method;
            }
            else
            {
              this.requiresWithExceptionMethod = method;
            }
          }
        }
        method = userContractType.GetMethod(Identifier.For("Ensures"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String);
        if (method != null) this.ensuresMethod = method;
        method = userContractType.GetMethod(Identifier.For("EnsuresOnThrow"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String, SystemTypes.Exception);
        if (method != null) this.ensuresOnThrowMethod = method;
        method = userContractType.GetMethod(Identifier.For("Invariant"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String);
        if (method != null) this.invariantMethod = method;
        method = userContractType.GetMethod(Identifier.For("Assert"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String);
        if (method != null) this.assertMethod = method;
        method = userContractType.GetMethod(Identifier.For("Assume"), SystemTypes.Boolean, SystemTypes.String, SystemTypes.String);
        if (method != null) this.assumeMethod = method;

        // Need to make sure that the type ContractFailureKind is the one used in the user-supplied methods, which is not necessarily
        // the one that is defined in the assembly that defines the contract class. For instance, extracting/rewriting from a 4.0 assembly
        // but where the user-supplied assembly is pre-4.0.
        var mems = userContractType.GetMembersNamed(ContractNodes.ReportFailureName);
        TypeNode contractFailureKind = contractNodes.ContractFailureKind;
        //if (mems != null) 
        {
          foreach(var mem in mems){
            method = mem as Method;
            if (method == null) continue;
            if (method.Parameters.Count != 4) continue;
            if (method.Parameters[0].Type.Name != contractNodes.ContractFailureKind.Name) continue;
            if (method.Parameters[1].Type != SystemTypes.String) continue;
            if (method.Parameters[2].Type != SystemTypes.String) continue;
            if (method.Parameters[3].Type != SystemTypes.Exception) continue;
            this.failureMethod = method;
            contractFailureKind = method.Parameters[0].Type;
            break;
          }
        }

        if (this.failureMethod == null) 
        {
          mems = userContractType.GetMembersNamed(ContractNodes.RaiseContractFailedEventName);
          // if (mems != null) 
          {
            foreach (var mem in mems) {
              method = mem as Method;
              if (method == null) continue;
              if (method.Parameters.Count != 4) continue;
              if (method.Parameters[0].Type.Name.UniqueIdKey != contractNodes.ContractFailureKind.Name.UniqueIdKey) continue;
              if (method.Parameters[1].Type != SystemTypes.String) continue;
              if (method.Parameters[2].Type != SystemTypes.String) continue;
              if (method.Parameters[3].Type != SystemTypes.Exception) continue;
              this.raiseFailureEventMethod = method;
              contractFailureKind = method.Parameters[0].Type;
              break;
            }
          }
        } else {
          method = userContractType.GetMethod(ContractNodes.RaiseContractFailedEventName, contractFailureKind, SystemTypes.String, SystemTypes.String, SystemTypes.Exception);
          if (method != null) this.raiseFailureEventMethod = method;
        }
        if (this.raiseFailureEventMethod != null) { // either take all both RaiseContractFailedEvent and TriggerFailure or neither
          method = userContractType.GetMethod(ContractNodes.TriggerFailureName, contractFailureKind, SystemTypes.String, SystemTypes.String, SystemTypes.String, SystemTypes.Exception);
          if (method != null) this.triggerFailureMethod = method;
        }

      }
      #endregion Get the user-specified rewriter methods (optional) REVIEW!! Needs a lot of error handling

    }

 public static TypeNode FindType(AssemblyNode startingPoint, Identifier ns, Identifier name)
 {
     return startingPoint.GetType(ns, name, true);
 }

 /// <summary>
 /// This is used to reset the target platform information if mscorlib is specified as one of the
 /// reference assemblies or documented assemblies.
 /// </summary>
 /// <param name="assembly">The system assembly for the target platform (mscorlib)</param>
 private static void ResetMscorlib(AssemblyNode assembly)
 {
     TargetPlatform.Clear();
     CoreSystemTypes.Clear();
     CoreSystemTypes.SystemAssembly = assembly;
     CoreSystemTypes.Initialize(true, false);
 }

 public virtual AssemblyNode VisitAssembly(AssemblyNode assembly)
 {
     if (assembly == null) return null;
     this.VisitModule(assembly);
     assembly.ModuleAttributes = this.VisitAttributeList(assembly.ModuleAttributes);
     assembly.SecurityAttributes = this.VisitSecurityAttributeList(assembly.SecurityAttributes);
     return assembly;
 }