internal static Statement GenerateForLoop(Variable loopVariable, Expression lowerBound, Expression upperBound, Statement body)
        {
            Block bodyAsBlock = body as Block ?? new Block(new StatementList(body));
            Block init = new Block(new StatementList(2));
            Block increment = new Block(new StatementList(1));
            Block test = new Block(new StatementList(new Branch(
              new BinaryExpression(loopVariable, upperBound, NodeType.Lt), bodyAsBlock))); //, false, true, false)));

            init.Statements.Add(new AssignmentStatement(loopVariable, lowerBound));
            init.Statements.Add(new Branch(null, test));

            increment.Statements.Add(new AssignmentStatement(loopVariable, new BinaryExpression(loopVariable, Literal.Int32One, NodeType.Add)));

            Block forLoop = new Block(new StatementList(4));
            forLoop.Statements.Add(init);
            forLoop.Statements.Add(bodyAsBlock);
            forLoop.Statements.Add(increment);
            forLoop.Statements.Add(test);
            return forLoop;
        }

 public void SetToFalse(Variable v) {
   this.egraph[v] = this.False;
 }

 public static string Name(Variable v) 
 {
   Identifier name = v.Name;
   string nstr = (name == null)?"":name.Name;
   return String.Format("{0}({1})", nstr, v.UniqueKey);
 }

 protected override object VisitSizeOf(Variable dest, TypeNode value_type, Statement stat, object arg) {
   ExposureState estate=(ExposureState)arg; 
   estate.AssignNonPointer(dest);
   return arg;
 }

    protected override object VisitBinaryOperator(NodeType op, Variable dest, Variable operand1, Variable operand2, Statement stat, object arg) {
      ExposureState estate=(ExposureState)arg; 

//      estate.AssignBinary(dest, op, operand1, operand2);

      return arg;
    }

    protected override object VisitReturn(Variable var, Statement stat, object arg) {
      ExposureState estate=(ExposureState)arg;

      // TODO: see if returned value is supposed to be exposed or not and then what do we know about it?
      return arg;
    }

    protected override object VisitLoadField(Variable dest, Variable source, Field field, Statement stat, object arg) {
      ExposureState estate=(ExposureState)arg;

      // Check the receiver here only if one needs to be unpacked for read access
      //CheckReceiver(stat,source,estate);

      return arg;
    }

    protected override object VisitCall(Variable dest, Variable receiver, Method callee, ExpressionList arguments, bool virtcall, Statement stat, object arg) {
      ExposureState estate=(ExposureState)arg;

      if (callee.CciKind == Cci.CciMemberKind.FrameGuardGetter){
        // associate dest with receiver, because unpack is going to happen with dest as receiver
        estate.AssignFrameFor(dest,receiver,callee.DeclaringType); // receiver could be a subtype of the type that the frame guard is for
      }else if (callee == UnpackMethod){
        if(estate.IsFrameExposable(receiver)) {
          // BUGBUG: Using CopyVariable encodes the assumption that StartWritingTransitively returns itself!!! It may not!
          estate.CopyVariable(receiver,dest);
          estate.AssignFrameForExposed(dest);
        }else{
          TypeNode t = estate.LowerBoundOfObjectPointedToByFrame(receiver);
          if (t == null){ // BUGBUG: is this the same as it being Top?
            HandleError(stat, stat, Error.DontKnowIfCanExposeObject);
          }else{
            HandleError(stat, stat, Error.ExposingExposedObject);
          }
          return null;
        }
      }else if (callee == PackMethod){
        estate.AssignFrameForNotExposed(receiver);
      }else if (callee == IsExposableMethod){
        estate.AssignFunctionLink(ExposureState.EqIsExposableId,dest,receiver);
      }else if (callee == IsExposedMethod){
        estate.AssignEqIsExposed(dest,receiver);
      }else if (callee == AssertMethod){
        Variable v = arguments[0] as Variable;
        if (v != null && estate.IsFalse(v))
          return null;
      }

      // Push possible exceptions to handlers.
      for(int i=0;i<callee.Contract.Ensures.Count;i++){
        EnsuresExceptional e=callee.Contract.Ensures[i] as EnsuresExceptional;
        if(e!=null){
          ExposureState newnn=new ExposureState(estate);
          newnn.currentException=e.Type;
          ExposureChecker.PushExceptionState(ExposureChecker.currBlock,newnn);
        }
      }

      return arg;
    }

 public void AssignFrameForNotExposed(Variable guardVariable){
   ISymValue guard = this.egraph[guardVariable];
   ISymValue guardTypeObject = this.egraph[StaticTypeOf,guard];
   Lattice.AVal guardsType = (Lattice.AVal)this.egraph[guardTypeObject];
   ISymValue guardedObject = this.egraph[FrameFor, guard];
   this.egraph[guardedObject] = guardsType;
 }

 public bool IsFrameExposable(Variable guardVariable){
   ISymValue guard = this.egraph[guardVariable];
   ISymValue guardedObject = this.egraph[FrameFor, guard];
   ISymValue guardTypeObject = this.egraph[StaticTypeOf,guard];
   Lattice.AVal guardsType = (Lattice.AVal)this.egraph[guardTypeObject];
   Lattice.AVal guardedObjectsType = (Lattice.AVal)this.egraph[guardedObject];
   return guardsType.lowerBound == guardedObjectsType.lowerBound;
 }

 public void AssignFrameForExposable(Variable guardVariable){
   ISymValue guard = this.egraph[guardVariable];
   this.AssignFrameForExposable(guard);
 }

 public void AssignFrameFor(Variable dest, Variable source, TypeNode t) {
   ISymValue guard = this.egraph.FreshSymbol();
   ISymValue guardedObject = this.egraph[source];
   this.egraph[dest] = guard;
   this.egraph[FrameFor, guard] = guardedObject;
   ISymValue fresh = this.egraph.FreshSymbol();
   this.egraph[fresh] = new Lattice.AVal(t,t);
   this.egraph[StaticTypeOf, guard] = fresh;
 }

 public void CopyVariable(Variable source, Variable dest) {
   this.egraph[dest] = this.egraph[source];
 }

 public void AssignNonPointer(Variable v) {
   this.egraph.Eliminate(v);
 }

 public bool IsFalse(Variable v){
   return this.egraph[v] == this.False;
 }

    protected override object VisitLoadConstant(Variable dest, Literal source, Statement stat, object arg) 
    {
      ExposureState estate=(ExposureState)arg;

      if (source == Literal.False){
        estate.SetToFalse(dest);
      }

      return arg;
    }

    /// <summary>
    /// Note: casts don't require a non-null argument. null value casts always succeed.
    /// </summary>
    protected override object VisitCastClass(Variable dest, TypeNode type, Variable source, Statement stat, object arg) {
      ExposureState estate=(ExposureState)arg;

      // acts like a copy retaining null status
      estate.CopyVariable(source, dest);
      return arg;
    }

 public void AssignEqIsExposed(Variable dest, Variable operand) {
   ISymValue opval = this.egraph[operand];
   ISymValue sv = this.egraph.FreshSymbol();
   this.egraph[dest] = sv; // ?? Ask Manuel: Should it be the sv' that dest maps to that sv should be mapped to here?
   this.egraph[EqIsExposedId, opval] = sv;
 }

    protected override object VisitConstrainedCall(Variable dest, Variable receiver, Method callee, ExpressionList arguments, TypeNode constraint, Statement stat, object arg) {
      Reference rtype = receiver.Type as Reference;
      if (rtype != null && rtype.ElementType != null && !rtype.ElementType.IsValueType) {
        // instance could be a reference type that could be null.

        // BUGBUG: when we track address of, we need to check here that target is indeed non-null
      }
      return VisitCall(dest, receiver, callee, arguments, true, stat, arg);
    }

 public void AssignFunctionLink(Identifier func, Variable dest, Variable operand) {
   ISymValue opval = this.egraph[operand];
   ISymValue sv = this.egraph.FreshSymbol();
   this.egraph[dest] = sv; // ?? Ask Manuel: Should it be the sv' that dest maps to that sv should be mapped to here?
   this.egraph[func, opval] = sv;
 }