public Warning(int errorCode, string error, SourceContext context)
            : base(errorCode, error, context)
        {
            // F:
            Contract.Requires(error != null);

            this.IsWarning = true;
        }

        public override void VisitStatementList(StatementList statements)
        {
            if (statements == null) return;

            for (int i = 0; i < statements.Count; i++)
            {
                var stmt = statements[i];
                if (stmt == null) continue;

                if (stmt.SourceContext.IsValid)
                {
                    this.currentSourceContext = stmt.SourceContext;
                }

                this.Visit(stmt);
            }
        }

 public override Compilation GetDummyCompilationFor(string fileName){
   if (this.dummyCompilationFor == null) this.dummyCompilationFor = new Hashtable();
   WeakReference wref = (WeakReference)this.dummyCompilationFor[fileName];
   if (wref != null && wref.IsAlive) return (Compilation)wref.Target;
   string fContents = null;
   if (File.Exists(fileName)){
     StreamReader sr = new StreamReader(fileName);
     fContents = sr.ReadToEnd(); sr.Close();
   }
   Compilation compilation = new Compilation();
   compilation.CompilerParameters = this.GetDummyCompilerParameters();
   compilation.TargetModule = new Module();
   DocumentText docText = new DocumentText(new StringSourceText(fContents, true));
   SourceContext sctx = new SourceContext(Compiler.CreateSpecSharpDocument(fileName, 0, docText));
   compilation.CompilationUnits = new CompilationUnitList(new CompilationUnitSnippet(new Identifier(fileName), new ParserFactory(), sctx));
   compilation.CompilationUnits[0].Compilation = compilation;
   this.dummyCompilationFor[fileName] = new WeakReference(compilation);
   return compilation;
 }

        public Error(int errorCode, string error, SourceContext context)
        {
            Contract.Requires(error != null);

            if (context.IsValid)
            {
                // F: Why context.Document != null? Added the assumption
                Contract.Assume(context.Document != null);

                this.FileName = context.Document.Name;
            }
            else
            {
                this.FileName = " "; // non-empty to prevent VS/msbuild from prepending EXEC 
            }

            this.Line = context.StartLine;
            this.Column = context.StartColumn;
            this.ErrorNumber = "CC" + errorCode;
            this.ErrorText = error;
        }

        //public override Block VisitBlock(Block block) {
        //  if(block.Statements != null && block.Statements.Count == 1) {
        //    Return r = block.Statements[0] as Return;
        //    if(r != null) {
        //      Statement s = this.VisitReturn(r);
        //      Block retBlock = s as Block;
        //      if(retBlock != null) {
        //        block.Statements = retBlock.Statements;
        //        return block;
        //      } else {
        //        return base.VisitBlock(block);
        //      }
        //    } else {
        //      return base.VisitBlock(block);
        //    }
        //  } else {
        //    return base.VisitBlock(block);
        //  }
        //}

        public override Statement VisitReturn(Return Return)
        {
            if (Return == null)
            {
                return null;
            }

            returnCount++;
            this.lastReturnSourceContext = Return.SourceContext;

            StatementList stmts = new StatementList();

            Return.Expression = this.VisitExpression(Return.Expression);

            if (Return.Expression != null)
            {
                MethodCall mc = Return.Expression as MethodCall;
                if (mc != null && mc.IsTailCall)
                {
                    mc.IsTailCall = false;
                }

                var assgnmt = new AssignmentStatement(result, Return.Expression);

                assgnmt.SourceContext = Return.SourceContext;
                stmts.Add(assgnmt);
            }

            // the branch is a "leave" out of the try block that the body will be
            // in.
            var branch = new Branch(null, newExit, false, false, this.leaveExceptionBody);
            branch.SourceContext = Return.SourceContext;

            stmts.Add(branch);

            return new Block(stmts);
        }

        private StatementList GetContractClumpFromMoveNext(Method iteratorMethod, Method moveNext,
            ContractNodes contractNodes, StatementList contractInitializer, out SourceContext defaultSourceContext,
            ref HelperMethods.StackDepthTracker dupStackTracker,
            out AssumeBlock originalContractPosition)
        {
            Contract.Requires(moveNext != null);
            Contract.Requires(moveNext.Body != null);
            Contract.Requires(moveNext.Body.Statements != null);
            Contract.Requires(contractInitializer != null);
            Contract.Requires(iteratorMethod != null);

            var linkerVersion = 0;
            if (iteratorMethod.DeclaringType != null && iteratorMethod.DeclaringType.DeclaringModule != null)
            {
                linkerVersion = iteratorMethod.DeclaringType.DeclaringModule.LinkerMajorVersion;
            }

            var initialState = moveNext.IsAsync ? -1 : 0;
            moveNext.MoveNextStartState = initialState;
            originalContractPosition = null;
            int statementIndex;

            Contract.Assume(moveNext.Body != null);
            Contract.Assume(moveNext.Body.Statements != null);

            int blockIndex = ContractStartInMoveNext(this.contractNodes, moveNext, out statementIndex, iteratorMethod);

            Contract.Assert(statementIndex >= 0, "should follow from the postcondiiton");

            if (blockIndex < 0)
            {
                // Couldn't find state 0 in MoveNext method
                // This can happen if the iterator is trivial (like yield break; )
                defaultSourceContext = default(SourceContext);
                return null;
            }

            int beginning = blockIndex; // the block number in the body of movenext
            int sbeginning = statementIndex; // the statement no. in the beginnning block after the preamble
            int blast = -1;

            // the block number in the body of movenext, of the last block where there is a contract call
            int slast = -1; // the statement no. in the blast block

            // Next we move sbeginning past the preamble area
            sbeginning = MovePastPreamble(iteratorMethod, moveNext, beginning, sbeginning, contractInitializer,
                contractNodes, ref dupStackTracker);

            Contract.Assert(moveNext.Body != null, "should be provable");
            Contract.Assert(moveNext.Body.Statements != null, "should be provable");

            if (sbeginning < 0 ||
                !this.FindLastBlockWithContracts(moveNext.Body.Statements, beginning, out blast, out slast))
            {
                if (verbose)
                {
                    if (moveNext.Name != null)
                    {
                        Console.WriteLine("Method {0} doesnt have a contract method invocation at the right place.", moveNext.Name.Name);
                    }
                }

                defaultSourceContext = default(SourceContext);
                return null;
            }

            Block methodBody = moveNext.Body;
            Block lastBlock = methodBody.Statements[blast] as Block;
            SourceContext lastContractSourceContext;

            if (lastBlock != null)
            {
                lastContractSourceContext = lastBlock.SourceContext;
                // probably not a good context, what to do if one can't be found?
                if (lastBlock.Statements != null && 0 <= slast && slast < lastBlock.Statements.Count)
                {
                    if (lastBlock.Statements[slast] != null)
                    {
                        lastContractSourceContext = lastBlock.Statements[slast].SourceContext;
                    }
                }
            }
            else
            {
                lastContractSourceContext = default(SourceContext);
            }

            // TODO: check the clump is not in a try-catch block. 

            originalContractPosition = new AssumeBlock(new StatementList());
            StatementList result = HelperMethods.ExtractClump(
                moveNext.Body.Statements, beginning, sbeginning, blast,
                slast, assumeBlock: originalContractPosition);

            defaultSourceContext = lastContractSourceContext;
            return result;
        }

        private void ExtractContractsForMethod(Method method, object dummy)
        {
            Contract.Requires(method != null);

            RequiresList preconditions = null;
            EnsuresList postconditions = null;
            RequiresList validations = null;
            EnsuresList modelPostconditions = null;

            //Console.WriteLine("Extracting contract for method {0}", method.FullName);

            // set its contract so pure is properly handled.
            var methodContract = method.Contract = new MethodContract(method);

            try
            {
                if (method.IsAbstract /* && contractClass == null */)
                {
                    // Abstract methods cannot have a body, so nothing to extract
                    return;
                }

                TypeNode /*?*/ closure = null;
                bool possiblyAsync;
                if (IsIteratorOrAsyncMethodCandidate(method, out possiblyAsync))
                {
                    closure = FindClosureClass(method);
                    if (closure != null)
                    {
                        this.ProcessClosureClass(method, closure, possiblyAsync);
                        return;
                    }
                }

                if (method.Body == null || method.Body.Statements == null)
                    return;

                // Find first source context, use it if no better one is found on errors

                // if (method.Body != null && method.Body.Statements != null)
                {
                    if (this.verbose)
                    {
                        Console.WriteLine(method.FullName);
                    }

                    bool found = false;
                    for (int i = 0, n = method.Body.Statements.Count; i < n && !found; i++)
                    {
                        Block b = method.Body.Statements[i] as Block;
                        if (b != null)
                        {
                            for (int j2 = 0, m = b.Statements == null ? 0 : b.Statements.Count; j2 < m; j2++)
                            {
                                Contract.Assert(m == b.Statements.Count, "loop invariant not inferred");

                                Statement s = b.Statements[j2];
                                if (s != null)
                                {
                                    SourceContext sctx = s.SourceContext;
                                    if (sctx.IsValid)
                                    {
                                        found = true;
                                        // s.SourceContext = new SourceContext(); // wipe out the source context because this statement will no longer be the first one in the method body if there are any contract calls
                                        this.currentMethodSourceContext = sctx;
                                        if (this.verbose)
                                        {
                                            Console.WriteLine("block {0}, statement {1}: ({2},{3})", i, j2, sctx.StartLine, sctx.StartColumn);
                                        }

                                        break;
                                    }
                                }
                            }
                        }
                    }
                }

                Block contractInitializerBlock = new Block(new StatementList());
                Block postPreamble = null;

                HelperMethods.StackDepthTracker dupStackTracker = new HelperMethods.StackDepthTracker();

                var contractLocalAliasingThis = HelperMethods.ExtractPreamble(method, this.contractNodes,
                    contractInitializerBlock, out postPreamble, ref dupStackTracker, this.isVB);

                bool saveErrorFound = this.errorFound;
                this.errorFound = false;

                // Extract pre- and postconditions

                if (method.Body != null && method.Body.Statements != null)
                {
                    this.CheapAndDirty(method, ref preconditions, ref postconditions, ref validations,
                        ref modelPostconditions, contractInitializerBlock, ref dupStackTracker);

                    if (this.errorFound)
                    {
                        method.ClearBody();

//.........这里部分代码省略.........

            public void CheckInvariants(TypeNode t, InvariantList invariants)
            {
                Contract.Requires(invariants != null);

                this.assignmentFound = false;
                foreach (var i in invariants)
                {
                    if (i == null) continue;

                    this.lastSourceContext = i.SourceContext;
                    this.CurrentMethod = i;
                    
                    this.Visit(i);
                    
                    Contract.Assume(this.CurrentMethod != null);
                    
                    if (this.assignmentFound)
                    {
                        this.errorHandler(
                            new Error(1003,
                                "Malformed contract. Found Invariant after assignment in method '" + this.CurrentMethod.FullName + "'.", 
                                i.SourceContext));
                        
                        break;
                    }
                }
            }

    private static Statement WrapTryCatch(Method method, Statement statement)
    {
      Block afterCatches = new Block(new StatementList());
      Block tryBlock = new Block(new StatementList());
      Block blockAfterTryBody = new Block(null);
      tryBlock.Statements.Add(statement);
      tryBlock.Statements.Add(new Branch(null, afterCatches, false, true, true));
      tryBlock.Statements.Add(blockAfterTryBody);
      Block catchBlock = new Block(new StatementList());
      // emit code that pops the exception and fools fxcop
      Block branchTargetToFoolFxCop = new Block(null);
      var branch = new Branch(new Expression(NodeType.Pop), branchTargetToFoolFxCop);
      SourceContext hiddenContext = new SourceContext(HiddenDocument.Document);
      branch.SourceContext = hiddenContext;
      catchBlock.Statements.Add(branch);
      var rethrowStatement = new Throw();
      rethrowStatement.SourceContext = hiddenContext;
      rethrowStatement.NodeType = NodeType.Rethrow;
      catchBlock.Statements.Add(rethrowStatement);
      catchBlock.Statements.Add(branchTargetToFoolFxCop);
      var leave = new Branch(null, afterCatches, false, true, true);
      leave.SourceContext = hiddenContext;
      catchBlock.Statements.Add(leave);
      Block tryCatch = new Block(new StatementList());
      tryCatch.Statements.Add(tryBlock);
      tryCatch.Statements.Add(catchBlock);
      tryCatch.Statements.Add(afterCatches);

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

      ExceptionHandler exHandler = new ExceptionHandler();
      exHandler.TryStartBlock = tryBlock;
      exHandler.BlockAfterTryEnd = blockAfterTryBody;
      exHandler.HandlerStartBlock = catchBlock;
      exHandler.BlockAfterHandlerEnd = afterCatches;
      exHandler.FilterType = SystemTypes.Exception;
      exHandler.HandlerType = NodeType.Catch;
      method.ExceptionHandlers.Add(exHandler);

      return tryCatch;
    }

    private bool ParseStatement(Block/*!*/ block) {
      //parse instructions and put in expression tree until an assignment, void call, branch target, or branch is encountered
      StatementList statementList = block.Statements;
      Expression expr = null;
      Statement statement = null;
      bool transferStatement = false;
      int startingAddress = 0;
#if !FxCop
      SourceContext sourceContext = new SourceContext();
      sourceContext.StartPos = this.counter;
#endif
#if !ROTOR
      if (this.method.contextForOffset != null){
        object sctx = this.method.contextForOffset[this.counter+1];
        if (sctx != null) sourceContext = (SourceContext)sctx;
      }
#endif
      while (true){
        bool isStatement = false;
        startingAddress = this.counter+1; //Add one so that it is never zero (the latter means no entry to the TrivialHashtable)
#if FxCop || ILOFFSETS
        this.ilOffset = this.counter;
        this.opCode = this.GetOpCode();
#else
        OpCode opCode = this.GetOpCode();
#endif
#if FxCop
        if (this.handlerMap.TryGetValue(this.ilOffset, out expr)){
          expr.sourceContext = sourceContext;
          expr.ILOffset = this.ilOffset;
          this.operandStack.Push(expr);
        }
#endif
        switch (opCode){
          case OpCode.Nop: statement = new Statement(NodeType.Nop); goto done;
          case OpCode.Break: statement = new Statement(NodeType.DebugBreak); goto done;
          case OpCode.Ldarg_0: expr = this.Parameters(0); break;
          case OpCode.Ldarg_1: expr = this.Parameters(1); break;
          case OpCode.Ldarg_2: expr = this.Parameters(2); break;
          case OpCode.Ldarg_3: expr = this.Parameters(3); break;
          case OpCode.Ldloc_0: expr = this.locals[0]; break;
          case OpCode.Ldloc_1: expr = this.locals[1]; break;
          case OpCode.Ldloc_2: expr = this.locals[2]; break;
          case OpCode.Ldloc_3: expr = this.locals[3]; break;
          case OpCode.Stloc_0: statement = new AssignmentStatement(this.locals[0], PopOperand()); goto done;
          case OpCode.Stloc_1: statement = new AssignmentStatement(this.locals[1], PopOperand()); goto done;
          case OpCode.Stloc_2: statement = new AssignmentStatement(this.locals[2], PopOperand()); goto done;
          case OpCode.Stloc_3: statement = new AssignmentStatement(this.locals[3], PopOperand()); goto done;
          case OpCode.Ldarg_S: expr = this.Parameters(this.GetByte()); break;
          case OpCode.Ldarga_S: expr = SetType(new UnaryExpression(this.Parameters(this.GetByte()), NodeType.AddressOf)); break;
          case OpCode.Starg_S: statement = new AssignmentStatement(this.Parameters(this.GetByte()), PopOperand()); goto done;
          case OpCode.Ldloc_S: expr = this.locals[this.GetByte()]; break;
          case OpCode.Ldloca_S: expr = SetType(new UnaryExpression(this.locals[this.GetByte()], NodeType.AddressOf)); break;
          case OpCode.Stloc_S: statement = new AssignmentStatement(this.locals[this.GetByte()], PopOperand()); goto done;
          case OpCode.Ldnull: expr = new Literal(null, CoreSystemTypes.Object); break;
          case OpCode.Ldc_I4_M1: expr = new Literal(-1, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_0: expr = new Literal(0, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_1: expr = new Literal(1, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_2: expr = new Literal(2, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_3: expr = new Literal(3, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_4: expr = new Literal(4, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_5: expr = new Literal(5, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_6: expr = new Literal(6, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_7: expr = new Literal(7, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_8: expr = new Literal(8, CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4_S: expr = new Literal((int)this.GetSByte(), CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I4: expr = new Literal(this.GetInt32(), CoreSystemTypes.Int32); break;
          case OpCode.Ldc_I8: expr = new Literal(this.GetInt64(), CoreSystemTypes.Int64); break;
          case OpCode.Ldc_R4: expr = new Literal(this.GetSingle(), CoreSystemTypes.Single); break;
          case OpCode.Ldc_R8: expr = new Literal(this.GetDouble(), CoreSystemTypes.Double); break;
          case OpCode.Dup: statement = new ExpressionStatement(new Expression(NodeType.Dup)); goto done;
          case OpCode.Pop: statement = new ExpressionStatement(new UnaryExpression(PopOperand(), NodeType.Pop)); goto done;
          case OpCode.Jmp: expr = this.ParseCall(NodeType.Jmp, out isStatement); if (isStatement) goto done; break;
          case OpCode.Call: expr = this.ParseCall(NodeType.Call, out isStatement); if (isStatement) goto done; break;
          case OpCode.Calli: expr = this.ParseCalli(out isStatement); if (isStatement) goto done; break;
          case OpCode.Ret:
            Expression retVal = BodyParser.TypeIsVoid(this.method.ReturnType) ? null : PopOperand();
            statement = new Return(retVal); 
            transferStatement = true; goto done;
          case OpCode.Br_S: statement = this.ParseBranch(NodeType.Nop, 0, true, false); transferStatement = true; goto done;
          case OpCode.Brfalse_S: statement = this.ParseBranch(NodeType.LogicalNot, 1, true, false); transferStatement = true; goto done;
          case OpCode.Brtrue_S: statement = this.ParseBranch(NodeType.Nop, 1, true, false); transferStatement = true; goto done;
          case OpCode.Beq_S: statement = this.ParseBranch(NodeType.Eq, 2, true, false); transferStatement = true; goto done;
          case OpCode.Bge_S: statement = this.ParseBranch(NodeType.Ge, 2, true, false); transferStatement = true; goto done;
          case OpCode.Bgt_S: statement = this.ParseBranch(NodeType.Gt, 2, true, false); transferStatement = true; goto done;
          case OpCode.Ble_S: statement = this.ParseBranch(NodeType.Le, 2, true, false); transferStatement = true; goto done;
          case OpCode.Blt_S: statement = this.ParseBranch(NodeType.Lt, 2, true, false); transferStatement = true; goto done;
          case OpCode.Bne_Un_S: statement = this.ParseBranch(NodeType.Ne, 2, true, true); transferStatement = true; goto done;
          case OpCode.Bge_Un_S: statement = this.ParseBranch(NodeType.Ge, 2, true, true); transferStatement = true; goto done;
          case OpCode.Bgt_Un_S: statement = this.ParseBranch(NodeType.Gt, 2, true, true); transferStatement = true; goto done;
          case OpCode.Ble_Un_S: statement = this.ParseBranch(NodeType.Le, 2, true, true); transferStatement = true; goto done;
          case OpCode.Blt_Un_S: statement = this.ParseBranch(NodeType.Lt, 2, true, true); transferStatement = true; goto done;
          case OpCode.Br: statement = this.ParseBranch(NodeType.Nop, 0, false, false); transferStatement = true; goto done;
          case OpCode.Brfalse: statement = this.ParseBranch(NodeType.LogicalNot, 1, false, false); transferStatement = true; goto done;
          case OpCode.Brtrue: statement = this.ParseBranch(NodeType.Nop, 1, false, false); transferStatement = true; goto done;
          case OpCode.Beq: statement = this.ParseBranch(NodeType.Eq, 2, false, false); transferStatement = true; goto done;
          case OpCode.Bge: statement = this.ParseBranch(NodeType.Ge, 2, false, false); transferStatement = true; goto done;
          case OpCode.Bgt: statement = this.ParseBranch(NodeType.Gt, 2, false, false); transferStatement = true; goto done;
          case OpCode.Ble: statement = this.ParseBranch(NodeType.Le, 2, false, false); transferStatement = true; goto done;
          case OpCode.Blt: statement = this.ParseBranch(NodeType.Lt, 2, false, false); transferStatement = true; goto done;
//.........这里部分代码省略.........

    internal Instruction ParseInstruction(){
      if (this.counter >= this.size) 
        return null;
      int offset = this.counter;
#if !ROTOR
      if (this.method.contextForOffset != null){
        object sctx = this.method.contextForOffset[offset+1];
        if (sctx != null) this.sourceContext = (SourceContext)sctx;
      }
#endif
      object value = null;
      OpCode opCode = this.GetOpCode();    
      switch(opCode){
        case OpCode.Nop:
        case OpCode.Break: 
          break;
        case OpCode.Ldarg_0: value = this.Parameters(0); break;
        case OpCode.Ldarg_1: value = this.Parameters(1); break;
        case OpCode.Ldarg_2: value = this.Parameters(2); break; 
        case OpCode.Ldarg_3: value = this.Parameters(3); break;
        case OpCode.Ldloc_0: value = this.locals[0]; break;
        case OpCode.Ldloc_1: value = this.locals[1]; break;
        case OpCode.Ldloc_2: value = this.locals[2]; break;
        case OpCode.Ldloc_3: value = this.locals[3]; break;
        case OpCode.Stloc_0: value = this.locals[0]; break;
        case OpCode.Stloc_1: value = this.locals[1]; break;
        case OpCode.Stloc_2: value = this.locals[2]; break;
        case OpCode.Stloc_3: value = this.locals[3]; break;
        case OpCode.Ldarg_S:  
        case OpCode.Ldarga_S:
        case OpCode.Starg_S:
          value = this.Parameters(this.GetByte()); break;
        case OpCode.Ldloc_S:
        case OpCode.Ldloca_S:
        case OpCode.Stloc_S:
          value = this.locals[this.GetByte()]; break;
        case OpCode.Ldnull: 
          break;
        case OpCode.Ldc_I4_M1: value = (Int32)(-1); break;
        case OpCode.Ldc_I4_0: value = (Int32)0; break;
        case OpCode.Ldc_I4_1: value = (Int32)1; break;
        case OpCode.Ldc_I4_2: value = (Int32)2; break;
        case OpCode.Ldc_I4_3: value = (Int32)3; break;
        case OpCode.Ldc_I4_4: value = (Int32)4; break;
        case OpCode.Ldc_I4_5: value = (Int32)5; break;
        case OpCode.Ldc_I4_6: value = (Int32)6; break;
        case OpCode.Ldc_I4_7: value = (Int32)7; break;
        case OpCode.Ldc_I4_8: value = (Int32)8; break;
        case OpCode.Ldc_I4_S: value = (Int32)this.GetSByte(); break;
        case OpCode.Ldc_I4: value = this.GetInt32(); break;
        case OpCode.Ldc_I8: value = this.GetInt64(); break;
        case OpCode.Ldc_R4: value = this.GetSingle(); break;
        case OpCode.Ldc_R8: value = this.GetDouble(); break;
        case OpCode.Dup:
        case OpCode.Pop: 
          break;
        case OpCode.Jmp: 
        case OpCode.Call:
          value = (Method)this.GetMemberFromToken(); break;
        case OpCode.Calli: 
          value = (FunctionPointer)this.reader.GetCalliSignature(this.GetInt32()); break;
        case OpCode.Ret: break;
        case OpCode.Br_S:
        case OpCode.Brfalse_S:
        case OpCode.Brtrue_S:
        case OpCode.Beq_S:
        case OpCode.Bge_S:
        case OpCode.Bgt_S:
        case OpCode.Ble_S:
        case OpCode.Blt_S:
        case OpCode.Bne_Un_S:
        case OpCode.Bge_Un_S:
        case OpCode.Bgt_Un_S:
        case OpCode.Ble_Un_S:
        case OpCode.Blt_Un_S:
          value = this.counter + 1 + this.GetSByte(); break;
        case OpCode.Br:
        case OpCode.Brfalse:
        case OpCode.Brtrue:
        case OpCode.Beq:
        case OpCode.Bge:
        case OpCode.Bgt:
        case OpCode.Ble:
        case OpCode.Blt:
        case OpCode.Bne_Un:
        case OpCode.Bge_Un:
        case OpCode.Bgt_Un:
        case OpCode.Ble_Un:
        case OpCode.Blt_Un:
          value = this.counter + 4 + this.GetInt32(); break;
        case OpCode.Switch: value = this.ParseSwitchInstruction(); break;        
        case OpCode.Ldind_I1: 
        case OpCode.Ldind_U1:
        case OpCode.Ldind_I2:
        case OpCode.Ldind_U2:
        case OpCode.Ldind_I4:
        case OpCode.Ldind_U4:
        case OpCode.Ldind_I8:
        case OpCode.Ldind_I:
        case OpCode.Ldind_R4:
//.........这里部分代码省略.........

        private void CopyAbbreviatorContracts(Method targetMethod, Method abbreviatorMethodInstance,
            Expression targetObject, ExpressionList actuals, RequiresList Preconditions, EnsuresList Postconditions,
            SourceContext useSite, RequiresList validations, Block contractInitializer)
        {
            Contract.Requires(validations != null);

            // make sure to have extracted contracts from the abbreviator method prior
            if (abbreviatorMethodInstance.DeclaringType.DeclaringModule == targetMethod.DeclaringType.DeclaringModule)
            {
                var abbrevMethod = abbreviatorMethodInstance;

                while (abbrevMethod.Template != null)
                {
                    abbrevMethod = abbrevMethod.Template;
                }

                this.VisitMethod(abbrevMethod);
            }

            if (abbreviatorMethodInstance.Contract == null) return;

            var copier = new AbbreviationDuplicator(abbreviatorMethodInstance, targetMethod, this.contractNodes,
                abbreviatorMethodInstance, targetObject, actuals);

            var abbrevContract = HelperMethods.DuplicateContractAndClosureParts(copier, targetMethod,
                abbreviatorMethodInstance, this.contractNodes, true);

            if (abbrevContract == null) return;

            if (HelperMethods.IsNonTrivial(abbrevContract.ContractInitializer))
            {
                contractInitializer.Statements.Add(abbrevContract.ContractInitializer);
            }

            MoveAbbreviatorRequires(targetMethod, abbrevContract.Requires, Preconditions, validations, useSite);
            MoveAbbreviatorEnsures(targetMethod, abbrevContract.Ensures, Postconditions, useSite);
        }

        internal static bool FindContext(Block currentClump, SourceContext initialSourceContext, out SourceContext sctx)
        {
            sctx = initialSourceContext;

            if (currentClump == null || currentClump.Statements == null || currentClump.Statements.Count <= 0)
                return false;

            for (int i = 0, n = currentClump.Statements.Count; i < n; i++)
            {
                Block b = currentClump.Statements[i] as Block;
                
                if (b == null || b.Statements == null || b.Statements.Count <= 0) continue;
                
                for (int j = 0, m = b.Statements.Count; j < m; j++)
                {
                    Statement s = b.Statements[j];
                    if (s == null) continue;

                    if (s.NodeType != NodeType.Nop
                        // these are the source contexts the compiler puts in that correspond to things like method declarations, etc.
                        && s.SourceContext.IsValid)
                    {
                        sctx = s.SourceContext;
                        return true;
                    }
                }
            }

            return false;
        }

        private bool ExtractFromClump(StatementList contractClump, Method method, GatherLocals gatherLocals,
            RequiresList Preconditions, EnsuresList Postconditions, RequiresList validations,
            EnsuresList modelPostconditions, SourceContext defaultContext, Method originalMethod,
            Block contractInitializer, ref HelperMethods.StackDepthTracker dupStackTracker)
        {
            // set the state so that the contract clump is used for extraction (as opposed to the method body as it used to)
            StatementList stmts = contractClump;

            int beginning = 0;
            int n = stmts.Count;
            int seginning = HelperMethods.FindNextRealStatement(((Block) stmts[beginning]).Statements, 0);

            bool endContractFound = false;
            bool postConditionFound = false;

            SourceContext currentSourceContext;

            for (int i = beginning; i < n; i++)
            {
                Block b = (Block) stmts[i];
                if (b == null) continue;

                for (int j = 0, m = b.Statements == null ? 0 : b.Statements.Count; j < m; j++)
                {
                    if (dupStackTracker.IsValid && dupStackTracker.Depth >= 0)
                    {
                        b.Statements[j] = dupStackTracker.Visit(b.Statements[j]);
                    }

                    Statement s = b.Statements[j];
                    if (s == null) continue;

                    Block currentClump;
                    Throw t = null;
                    t = s as Throw;

                    Method calledMethod = HelperMethods.IsMethodCall(s);
                    if ((t != null ||
                         (calledMethod != null &&
                          calledMethod.DeclaringType != null &&
                          calledMethod.DeclaringType != this.contractNodes.ContractClass &&
                          HelperMethods.IsVoidType(calledMethod.ReturnType) &&
                          !this.contractNodes.IsContractOrValidatorOrAbbreviatorMethod(calledMethod))))
                    {
                        // Treat throw statements as (part of) a precondition

                        // don't accept "throw ..." unless it comes in the "precondition section"
                        // then treat the current clump as a precondition, but need to massage it a bit:
                        // all branches to the block just after the throw should be modified to be branches to
                        // a new manufactured block that sets a fresh local to "true". The
                        // throw itself should be changed to set the same local to "false". That way the
                        // clump can be treated as the value of precondition (because the branch polarity has
                        // already been negated as part of the code gen).

                        // This test was supposed to be a sanity check that the current block contained
                        // only "throw ..." or else "nop; throw ...". But I've also seen "ThrowHelper.Throw(...); nop",
                        // so I'm just going to comment this out for now.
                        //if (!((m == 1 && j == 0) || (m == 2 && j == 1))) {
                        //  Preconditions = new RequiresList();
                        //  Postconditions = new EnsuresList();
                        //  return; // throw new ExtractorException();
                        //}

                        Expression exception;

                        // The clump being extracted may contain code/blocks that represent (part of)
                        // the expression that is being thrown (if the original throw expression had
                        // control flow in it from boolean expressions and/or ternary expressions).

                        b.Statements[j] = null; // wipe out throw statement

                        currentClump = new Block(HelperMethods.ExtractClump(stmts, beginning, seginning, i, j));
                        int currentClumpLength = i - beginning + 1;

                        // there better be a next block because that must have been the target for all of the branches
                        // that didn't cause the throw to happen
                        if (!(i < n - 1))
                        {
                            this.HandleError(method, 1027, "Malformed contract.", s.SourceContext);
                            return false;
                        }

                        Block nextBlock = (Block) stmts[i + 1]; // cast succeeds because body is clump
                        Local valueOfPrecondition = new Local(Identifier.For("_preConditionHolds"), SystemTypes.Boolean);
                        Block preconditionHolds = new Block(new StatementList(new AssignmentStatement(valueOfPrecondition, Literal.True)));

                        ReplaceBranchTarget rbt = new ReplaceBranchTarget(nextBlock, preconditionHolds);
                        rbt.VisitBlock(currentClump);

                        int ILOffset;
                        CountPopExpressions cpe = new CountPopExpressions();
                        currentSourceContext = s.SourceContext;
                        cpe.Visit(s);

                        if (0 < cpe.PopOccurrences)
                        {
                            // then there is a set of blocks that represent the exception: the Reader
                            // was not able to decompile it back into an expression. Extract the set
                            // from the current clump and make it into a block expression

//.........这里部分代码省略.........

 public ContractAssumeAssertStatement(Expression expression, SourceContext sctx, string sourceText)
     : base(expression, sctx)
 {
     this.SourceText = sourceText;
 }

    private Method CreateWrapperMethod(bool virtcall, TypeNode virtcallConstraint, Method templateMethod, TypeNode templateType, TypeNode wrapperType, Method methodWithContract, Method instanceMethod, SourceContext callingContext)
    {
      bool isProtected = IsProtected(templateMethod);
      Identifier name = templateMethod.Name;
      if (virtcall) {
        if (virtcallConstraint != null) {
          name = Identifier.For("CV$" + name.Name);
        }
        else {
          name = Identifier.For("V$" + name.Name);
        }
      }
      else {
        name = Identifier.For("NV$" + name.Name);
      }
      Duplicator dup = new Duplicator(this.assemblyBeingRewritten, wrapperType);
      TypeNodeList typeParameters = null;
      TypeNodeList typeParameterFormals = new TypeNodeList();
      TypeNodeList typeParameterActuals = new TypeNodeList();

      if (templateMethod.TemplateParameters != null) {
        dup.FindTypesToBeDuplicated(templateMethod.TemplateParameters);
        typeParameters = dup.VisitTypeParameterList(templateMethod.TemplateParameters);
        for (int i = 0; i < typeParameters.Count; i++) {
          typeParameterFormals.Add(typeParameters[i]);
          typeParameterActuals.Add(templateMethod.TemplateParameters[i]);
        }
      }
      ITypeParameter constraintTypeParam = null;
      if (virtcallConstraint != null) {
        if (typeParameters == null) { typeParameters = new TypeNodeList(); }
        var constraint = templateMethod.DeclaringType;
        var classConstraint = constraint as Class;
        if (classConstraint != null) {
          var classParam = new MethodClassParameter();
          classParam.BaseClass = classConstraint;
          classParam.Name = Identifier.For("TC");
          classParam.DeclaringType = wrapperType;
          typeParameters.Add(classParam);
          constraintTypeParam = classParam;
        }
        else {
          var mtp = new MethodTypeParameter();
          Interface intf = constraint as Interface;
          if (intf != null) {
            mtp.Interfaces.Add(intf);
          }
          mtp.Name = Identifier.For("TC");
          mtp.DeclaringType = wrapperType;
          typeParameters.Add(mtp);
          constraintTypeParam = mtp;
        }
      }
      var consolidatedTemplateTypeParameters = templateType.ConsolidatedTemplateParameters;
      if (consolidatedTemplateTypeParameters != null && consolidatedTemplateTypeParameters.Count > 0) {
        var consolidatedWrapperTypeParameters = wrapperType.ConsolidatedTemplateParameters;
        for (int i = 0; i < consolidatedTemplateTypeParameters.Count; i++) {
          typeParameterFormals.Add(consolidatedWrapperTypeParameters[i]);
          typeParameterActuals.Add(consolidatedTemplateTypeParameters[i]);
        }
      }
      Specializer spec = null;
      if (typeParameterActuals.Count > 0) {
        spec = new Specializer(this.assemblyBeingRewritten, typeParameterActuals, typeParameterFormals);
      }
      var parameters = new ParameterList();
      var asTypeConstraintTypeParam = constraintTypeParam as TypeNode;

      if (!isProtected && !templateMethod.IsStatic) {
        TypeNode thisType = GetThisTypeInstance(templateType, wrapperType, asTypeConstraintTypeParam);
        parameters.Add(new Parameter(Identifier.For("@this"), thisType));
      }
      for (int i = 0; i < templateMethod.Parameters.Count; i++) {
        parameters.Add((Parameter)dup.VisitParameter(templateMethod.Parameters[i]));
      }
      var retType = dup.VisitTypeReference(templateMethod.ReturnType);
      if (spec != null) {
        parameters = spec.VisitParameterList(parameters);
        retType = spec.VisitTypeReference(retType);
      }

      var wrapperMethod = new Method(wrapperType, null, name, parameters, retType, null);
      RewriteHelper.TryAddCompilerGeneratedAttribute(wrapperMethod);

      if (isProtected) {
        wrapperMethod.Flags = templateMethod.Flags & ~MethodFlags.Abstract;
        wrapperMethod.CallingConvention = templateMethod.CallingConvention;
      }
      else {
        wrapperMethod.Flags |= MethodFlags.Static | MethodFlags.Assembly;
      }
      if (constraintTypeParam != null) {
        constraintTypeParam.DeclaringMember = wrapperMethod;
      }
      if (typeParameters != null) {
        if (spec != null) {
          typeParameters = spec.VisitTypeParameterList(typeParameters);
        }
        wrapperMethod.IsGeneric = true;
        wrapperMethod.TemplateParameters