GRExprEngine.cpp

    ValueState* St = GetState(*DI);
    RVal L = GetRVal(St, Callee);

    // FIXME: Add support for symbolic function calls (calls involving
    //  function pointer values that are symbolic).
    
    // Check for undefined control-flow or calls to NULL.
    
    if (L.isUndef() || isa<lval::ConcreteInt>(L)) {      
      NodeTy* N = Builder->generateNode(CE, St, *DI);
      
      if (N) {
        N->markAsSink();
        BadCalls.insert(N);
      }
      
      continue;
    }
    
    // Check for the "noreturn" attribute.
    
    SaveAndRestore<bool> OldSink(Builder->BuildSinks);
    
    if (isa<lval::FuncVal>(L)) {      
      
      FunctionDecl* FD = cast<lval::FuncVal>(L).getDecl();
      
      if (FD->getAttr<NoReturnAttr>())
        Builder->BuildSinks = true;
      else {
        // HACK: Some functions are not marked noreturn, and don't return.
        //  Here are a few hardwired ones.  If this takes too long, we can
        //  potentially cache these results.
        const char* s = FD->getIdentifier()->getName();
        unsigned n = strlen(s);
        
        switch (n) {
          default:
            break;
            
          case 4:
            if (!memcmp(s, "exit", 4)) Builder->BuildSinks = true;
            break;

          case 5:
            if (!memcmp(s, "panic", 5)) Builder->BuildSinks = true;
            break;
          
          case 6:
            if (!memcmp(s, "Assert", 6)) Builder->BuildSinks = true;
            break;
          
          case 7:
            if (!memcmp(s, "assfail", 7)) Builder->BuildSinks = true;
            break;
            
          case 8:
            if (!memcmp(s ,"db_error", 8)) Builder->BuildSinks = true;
            break;
            
          case 14:
            if (!memcmp(s, "dtrace_assfail", 14)) Builder->BuildSinks = true;
            break;
        }
        
      }
    }
    
    // Evaluate the call.

    if (isa<lval::FuncVal>(L)) {
      
      IdentifierInfo* Info = cast<lval::FuncVal>(L).getDecl()->getIdentifier();
      
      if (unsigned id = Info->getBuiltinID())
        switch (id) {
          case Builtin::BI__builtin_expect: {
            // For __builtin_expect, just return the value of the subexpression.
            assert (CE->arg_begin() != CE->arg_end());            
            RVal X = GetRVal(St, *(CE->arg_begin()));
            MakeNode(Dst, CE, *DI, SetRVal(St, CE, X));
            continue;            
          }
            
          default:
            break;
        }
    }

    // Check any arguments passed-by-value against being undefined.

    bool badArg = false;
    
    for (CallExpr::arg_iterator I = CE->arg_begin(), E = CE->arg_end();
         I != E; ++I) {

      if (GetRVal(GetState(*DI), *I).isUndef()) {        
        NodeTy* N = Builder->generateNode(CE, GetState(*DI), *DI);
      
        if (N) {
          N->markAsSink();
          UndefArgs[N] = *I;
        }
        
        badArg = true;
        break;
      }
    }
    
    if (badArg)
      continue;        

    // Dispatch to the plug-in transfer function.      
    
    unsigned size = Dst.size();
    SaveOr OldHasGen(Builder->HasGeneratedNode);
    EvalCall(Dst, CE, L, *DI);
    
    // Handle the case where no nodes where generated.  Auto-generate that
    // contains the updated state if we aren't generating sinks.
    
    if (!Builder->BuildSinks && Dst.size() == size &&
        !Builder->HasGeneratedNode)
      MakeNode(Dst, CE, *DI, St);
  }
}

//===----------------------------------------------------------------------===//
// Transfer function: Objective-C message expressions.
//===----------------------------------------------------------------------===//

void GRExprEngine::VisitObjCMessageExpr(ObjCMessageExpr* ME, NodeTy* Pred,
                                        NodeSet& Dst){
  
  VisitObjCMessageExprArgHelper(ME, ME->arg_begin(), ME->arg_end(),
                                Pred, Dst);
}  

void GRExprEngine::VisitObjCMessageExprArgHelper(ObjCMessageExpr* ME,
                                                 ObjCMessageExpr::arg_iterator AI,
                                                 ObjCMessageExpr::arg_iterator AE,
                                                 NodeTy* Pred, NodeSet& Dst) {
  if (AI == AE) {
    
    // Process the receiver.
    
    if (Expr* Receiver = ME->getReceiver()) {
      NodeSet Tmp;
      Visit(Receiver, Pred, Tmp);
      
      for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
        VisitObjCMessageExprDispatchHelper(ME, *NI, Dst);
      
      return;
    }
    
    VisitObjCMessageExprDispatchHelper(ME, Pred, Dst);
    return;
  }
  
  NodeSet Tmp;
  Visit(*AI, Pred, Tmp);
  
  ++AI;
  
  for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
    VisitObjCMessageExprArgHelper(ME, AI, AE, *NI, Dst);
}

void GRExprEngine::VisitObjCMessageExprDispatchHelper(ObjCMessageExpr* ME,
                                                      NodeTy* Pred,
                                                      NodeSet& Dst) {
  
  // FIXME: More logic for the processing the method call. 
  
  ValueState* St = GetState(Pred);
  
  if (Expr* Receiver = ME->getReceiver()) {
    
    RVal L = GetRVal(St, Receiver);
    
    // Check for undefined control-flow or calls to NULL.
    
    if (L.isUndef()) {
      NodeTy* N = Builder->generateNode(ME, St, Pred);
      
      if (N) {
        N->markAsSink();
        UndefReceivers.insert(N);
      }
      
      return;
    }
  }
  
  // Check for any arguments that are uninitialized/undefined.
  
  for (ObjCMessageExpr::arg_iterator I = ME->arg_begin(), E = ME->arg_end();
       I != E; ++I) {
    
    if (GetRVal(St, *I).isUndef()) {
      
      // Generate an error node for passing an uninitialized/undefined value
      // as an argument to a message expression.  This node is a sink.
      NodeTy* N = Builder->generateNode(ME, St, Pred);
      
      if (N) {
        N->markAsSink();
        MsgExprUndefArgs[N] = *I;
      }
      
      return;
    }    
  }    
  // Dispatch to plug-in transfer function.
  
  unsigned size = Dst.size();

  SaveAndRestore<bool> OldSink(Builder->BuildSinks);
  SaveOr OldHasGen(Builder->HasGeneratedNode);
 
  EvalObjCMessageExpr(Dst, ME, Pred);
  
  // Handle the case where no nodes where generated.  Auto-generate that
  // contains the updated state if we aren't generating sinks.
  
  if (!Builder->BuildSinks && Dst.size() == size && !Builder->HasGeneratedNode)
    MakeNode(Dst, ME, Pred, St);
}

//===----------------------------------------------------------------------===//
// Transfer functions: Miscellaneous statements.
//===----------------------------------------------------------------------===//

void GRExprEngine::VisitCast(Expr* CastE, Expr* Ex, NodeTy* Pred, NodeSet& Dst){
  
  NodeSet S1;
  QualType T = CastE->getType();
  
  if (T->isReferenceType())
    VisitLVal(Ex, Pred, S1);
  else
    Visit(Ex, Pred, S1);
  
  // Check for casting to "void".
  if (T->isVoidType()) {
    
    for (NodeSet::iterator I1 = S1.begin(), E1 = S1.end(); I1 != E1; ++I1)
      Dst.Add(*I1);

    return;
  }
  
  // FIXME: The rest of this should probably just go into EvalCall, and
  //   let the transfer function object be responsible for constructing
  //   nodes.
  
  QualType ExTy = Ex->getType();
  
  for (NodeSet::iterator I1 = S1.begin(), E1 = S1.end(); I1 != E1; ++I1) {
    NodeTy* N = *I1;
    ValueState* St = GetState(N);
    RVal V = GetRVal(St, Ex);

    // Unknown?
    
    if (V.isUnknown()) {
      Dst.Add(N);
      continue;
    }
    
    // Undefined?
    
    if (V.isUndef()) {
      MakeNode(Dst, CastE, N, SetRVal(St, CastE, V));
      continue;
    }
  
    // Check for casts from pointers to integers.
    if (T->isIntegerType() && IsPointerType(ExTy)) {
      unsigned bits = getContext().getTypeSize(ExTy);
    
      // FIXME: Determine if the number of bits of the target type is 
      // equal or exceeds the number of bits to store the pointer value.
      // If not, flag an error.
      
      V = nonlval::LValAsInteger::Make(BasicVals, cast<LVal>(V), bits);
      MakeNode(Dst, CastE, N, SetRVal(St, CastE, V));
      continue;
    }
    
    // Check for casts from integers to pointers.
    if (IsPointerType(T) && ExTy->isIntegerType())
      if (nonlval::LValAsInteger *LV = dyn_cast<nonlval::LValAsInteger>(&V)) {
        // Just unpackage the lval and return it.
        V = LV->getLVal();
        MakeNode(Dst, CastE, N, SetRVal(St, CastE, V));
        continue;
      }
    
    // All other cases.
    
    MakeNode(Dst, CastE, N, SetRVal(St, CastE, EvalCast(V, CastE->getType())));
  }
}

void GRExprEngine::VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst) {  
  VisitDeclStmtAux(DS, DS->getDecl(), Pred, Dst);
}

void GRExprEngine::VisitDeclStmtAux(DeclStmt* DS, ScopedDecl* D,
                                    NodeTy* Pred, NodeSet& Dst) {

  if (!D)
    return;
  
  if (!isa<VarDecl>(D)) {
    VisitDeclStmtAux(DS, D->getNextDeclarator(), Pred, Dst);
    return;
  }
  
  const VarDecl* VD = dyn_cast<VarDecl>(D);
  
  // FIXME: Add support for local arrays.
  if (VD->getType()->isArrayType()) {
    VisitDeclStmtAux(DS, D->getNextDeclarator(), Pred, Dst);
    return;
  }
  
  Expr* Ex = const_cast<Expr*>(VD->getInit());

  // FIXME: static variables may have an initializer, but the second
  //  time a function is called those values may not be current.
  NodeSet Tmp;

  if (Ex) Visit(Ex, Pred, Tmp);
  if (Tmp.empty()) Tmp.Add(Pred);
  
  for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {
      
    ValueState* St = GetState(*I);

    if (!Ex && VD->hasGlobalStorage()) {
      
      // Handle variables with global storage and no initializers.
      
      // FIXME: static variables may have an initializer, but the second
      //  time a function is called those values may not be current.
      
      
      // In this context, Static => Local variable.
      
      assert (!VD->getStorageClass() == VarDecl::Static ||
              !VD->isFileVarDecl());
      
      // If there is no initializer, set the value of the
      // variable to "Undefined".
      
      if (VD->getStorageClass() == VarDecl::Static) {
          
        // C99: 6.7.8 Initialization
        //  If an object that has static storage duration is not initialized
        //  explicitly, then: 
        //   —if it has pointer type, it is initialized to a null pointer; 
        //   —if it has arithmetic type, it is initialized to (positive or 
        //     unsigned) zero; 
        
        // FIXME: Handle structs.  Now we treat their values as unknown.

        QualType T = VD->getType();
        
        if (IsPointerType(T))
          St = SetRVal(St, lval::DeclVal(VD),
                       lval::ConcreteInt(BasicVals.getValue(0, T)));
        else if (T->isIntegerType())
          St = SetRVal(St, lval::DeclVal(VD),
                       nonlval::ConcreteInt(BasicVals.getValue(0, T)));          
          
        // FIXME: Handle structs.  Now we treat them as unknown.  What
        //  we need to do is treat their members as unknown.
      }
    }
    else {
      
      // FIXME: Handle structs.  Now we treat them as unknown.  What
      //  we need to do is treat their members as unknown.

      QualType T = VD->getType();

      if (IsPointerType(T) || T->isIntegerType()) {
        
        RVal V = Ex ? GetRVal(St, Ex) : UndefinedVal();
        
        if (Ex && V.isUnknown()) {
          
          // EXPERIMENTAL: "Conjured" symbols.

          unsigned Count = Builder->getCurrentBlockCount();
          SymbolID Sym = SymMgr.getConjuredSymbol(Ex, Count);
          
          V = IsPointerType(Ex->getType())
            ? cast<RVal>(lval::SymbolVal(Sym)) 
            : cast<RVal>(nonlval::SymbolVal(Sym));            
        }
        
        St = SetRVal(St, lval::DeclVal(VD), V);        
      }
    }

    // Create a new node.  We don't really need to create a new NodeSet
    // here, but it simplifies things and doesn't cost much.
    NodeSet Tmp2;    
    MakeNode(Tmp2, DS, *I, St);
    if (Tmp2.empty()) Tmp2.Add(*I);
    
    for (NodeSet::iterator I2=Tmp2.begin(), E2=Tmp2.end(); I2!=E2; ++I2)
      VisitDeclStmtAux(DS, D->getNextDeclarator(), *I2, Dst);
  }
}


/// VisitSizeOfAlignOfTypeExpr - Transfer function for sizeof(type).
void GRExprEngine::VisitSizeOfAlignOfTypeExpr(SizeOfAlignOfTypeExpr* Ex,
                                              NodeTy* Pred,
                                              NodeSet& Dst) {
  QualType T = Ex->getArgumentType();
  uint64_t amt;  
  
  if (Ex->isSizeOf()) {

    // FIXME: Add support for VLAs.
    if (!T.getTypePtr()->isConstantSizeType())
      return;
    
    // Some code tries to take the sizeof an ObjCInterfaceType, relying that
    // the compiler has laid out its representation.  Just report Unknown
    // for these.
    if (T->isObjCInterfaceType())
      return;
    
    amt = 1;  // Handle sizeof(void)
    
    if (T != getContext().VoidTy)
      amt = getContext().getTypeSize(T) / 8;
    
  }
  else  // Get alignment of the type.
    amt = getContext().getTypeAlign(T) / 8;
  
  MakeNode(Dst, Ex, Pred,
           SetRVal(GetState(Pred), Ex,
                   NonLVal::MakeVal(BasicVals, amt, Ex->getType())));  
}


void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
                                      NodeSet& Dst, bool asLVal) {

  switch (U->getOpcode()) {
      
    default:
      break;
      
    case UnaryOperator::Deref: {
      
      Expr* Ex = U->getSubExpr()->IgnoreParens();
      NodeSet Tmp;
      Visit(Ex, Pred, Tmp);
      
      for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {
        
        ValueState* St = GetState(*I);
        RVal location = GetRVal(St, Ex);
        
        if (asLVal)
          MakeNode(Dst, U, *I, SetRVal(St, U, location));
        else
          EvalLoad(Dst, Ex, *I, St, location);
      } 

      return;
    }

    case UnaryOperator::Plus: assert (!asLVal);  // FALL-THROUGH.
    case UnaryOperator::Extension: {
      
      // Unary "+" is a no-op, similar to a parentheses.  We still have places
      // where it may be a block-level expression, so we need to
      // generate an extra node that just propagates the value of the
      // subexpression.

      Expr* Ex = U->getSubExpr()->IgnoreParens();
      NodeSet Tmp;
      Visit(Ex, Pred, Tmp);
      
      for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {        
        ValueState* St = GetState(*I);
        MakeNode(Dst, U, *I, SetRVal(St, U, GetRVal(St, Ex)));
      }
      
      return;
    }
    
    case UnaryOperator::AddrOf: {
      
      assert (!asLVal);
      Expr* Ex = U->getSubExpr()->IgnoreParens();
      NodeSet Tmp;
      VisitLVal(Ex, Pred, Tmp);
     
      for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {        
        ValueState* St = GetState(*I);
        RVal V = GetRVal(St, Ex);
        St = SetRVal(St, U, V);
        MakeNode(Dst, U, *I, St);
      }

      return; 
    }
      
    case UnaryOperator::LNot:
    case UnaryOperator::Minus:
    case UnaryOperator::Not: {
      
      assert (!asLVal);
      Expr* Ex = U->getSubExpr()->IgnoreParens();
      NodeSet Tmp;
      Visit(Ex, Pred, Tmp);
      
      for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {        
        ValueState* St = GetState(*I);
        RVal V = GetRVal(St, Ex);
        
        if (V.isUnknownOrUndef()) {
          MakeNode(Dst, U, *I, SetRVal(St, U, V));
          continue;
        }
        
        switch (U->getOpcode()) {
          default:
            assert(false && "Invalid Opcode.");
            break;
            
          case UnaryOperator::Not:
            St = SetRVal(St, U, EvalComplement(cast<NonLVal>(V)));
            break;            
            
          case UnaryOperator::Minus:
            St = SetRVal(St, U, EvalMinus(U, cast<NonLVal>(V)));
            break;   
            
          case UnaryOperator::LNot:   
            
            // C99 6.5.3.3: "The expression !E is equivalent to (0==E)."
            //
            //  Note: technically we do "E == 0", but this is the same in the
            //    transfer functions as "0 == E".
            
            if (isa<LVal>(V)) {
              lval::ConcreteInt X(BasicVals.getZeroWithPtrWidth());
              RVal Result = EvalBinOp(BinaryOperator::EQ, cast<LVal>(V), X);
              St = SetRVal(St, U, Result);
            }
            else {
              nonlval::ConcreteInt X(BasicVals.getValue(0, Ex->getType()));
              RVal Result = EvalBinOp(BinaryOperator::EQ, cast<NonLVal>(V), X);
              St = SetRVal(St, U, Result);
            }
            
            break;
        }
        
        MakeNode(Dst, U, *I, St);
      }
      
      return;
    }
      
    case UnaryOperator::SizeOf: {
            
      QualType T = U->getSubExpr()->getType();
        
      // FIXME: Add support for VLAs.
      
      if (!T.getTypePtr()->isConstantSizeType())
        return;
        
      uint64_t size = getContext().getTypeSize(T) / 8;                
      ValueState* St = GetState(Pred);
      St = SetRVal(St, U, NonLVal::MakeVal(BasicVals, size, U->getType()));
        
      MakeNode(Dst, U, Pred, St);
      return;
    }
  }

  // Handle ++ and -- (both pre- and post-increment).

  assert (U->isIncrementDecrementOp());
  NodeSet Tmp;
  Expr* Ex = U->getSubExpr()->IgnoreParens();
  VisitLVal(Ex, Pred, Tmp);
  
  for (NodeSet::iterator I = Tmp.begin(), E = Tmp.end(); I!=E; ++I) {
    
    ValueState* St = GetState(*I);
    RVal V1 = GetRVal(St, Ex);
    
    // Perform a load.      
    NodeSet Tmp2;
    EvalLoad(Tmp2, Ex, *I, St, V1);

    for (NodeSet::iterator I2 = Tmp2.begin(), E2 = Tmp2.end(); I2!=E2; ++I2) {
        
      St = GetState(*I2);
      RVal V2 = GetRVal(St, Ex);
        
      // Propagate unknown and undefined values.      
      if (V2.isUnknownOrUndef()) {
        MakeNode(Dst, U, *I2, SetRVal(St, U, V2));
        continue;
      }
      
      // Handle all other values.
      
      BinaryOperator::Opcode Op = U->isIncrementOp() ? BinaryOperator::Add
                                                     : BinaryOperator::Sub;
      
      RVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U));      
      St = SetRVal(St, U, U->isPostfix() ? V2 : Result);

      // Perform the store.      
      EvalStore(Dst, U, *I2, St, V1, Result);
    }
  }
}

void GRExprEngine::VisitAsmStmt(AsmStmt* A, NodeTy* Pred, NodeSet& Dst) {
  VisitAsmStmtHelperOutputs(A, A->begin_outputs(), A->end_outputs(), Pred, Dst);
}  

void GRExprEngine::VisitAsmStmtHelperOutputs(AsmStmt* A,
                                             AsmStmt::outputs_iterator I,
                                             AsmStmt::outputs_iterator E,
                                             NodeTy* Pred, NodeSet& Dst) {
  if (I == E) {
    VisitAsmStmtHelperInputs(A, A->begin_inputs(), A->end_inputs(), Pred, Dst);
    return;
  }
  
  NodeSet Tmp;
  VisitLVal(*I, Pred, Tmp);
  
  ++I;
  
  for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
    VisitAsmStmtHelperOutputs(A, I, E, *NI, Dst);
}

void GRExprEngine::VisitAsmStmtHelperInputs(AsmStmt* A,
                                            AsmStmt::inputs_iterator I,
                                            AsmStmt::inputs_iterator E,
                                            NodeTy* Pred, NodeSet& Dst) {
  if (I == E) {
    
    // We have processed both the inputs and the outputs.  All of the outputs
    // should evaluate to LVals.  Nuke all of their values.
    
    // FIXME: Some day in the future it would be nice to allow a "plug-in"
    // which interprets the inline asm and stores proper results in the
    // outputs.
    
    ValueState* St = GetState(Pred);
    
    for (AsmStmt::outputs_iterator OI = A->begin_outputs(),
                                   OE = A->end_outputs(); OI != OE; ++OI) {
      
      RVal X = GetRVal(St, *OI);      
      assert (!isa<NonLVal>(X));  // Should be an Lval, or unknown, undef.
      
      if (isa<LVal>(X))
        St = SetRVal(St, cast<LVal>(X), UnknownVal());
    }
    
    MakeNode(Dst, A, Pred, St);
    return;
  }
  
  NodeSet Tmp;
  Visit(*I, Pred, Tmp);
  
  ++I;
  
  for (NodeSet::iterator NI = Tmp.begin(), NE = Tmp.end(); NI != NE; ++NI)
    VisitAsmStmtHelperInputs(A, I, E, *NI, Dst);
}

void GRExprEngine::EvalReturn(NodeSet& Dst, ReturnStmt* S, NodeTy* Pred) {
  assert (Builder && "GRStmtNodeBuilder must be defined.");
  
  unsigned size = Dst.size();  

  SaveAndRestore<bool> OldSink(Builder->BuildSinks);
  SaveOr OldHasGen(Builder->HasGeneratedNode);

  TF->EvalReturn(Dst, *this, *Builder, S, Pred);
  
  // Handle the case where no nodes where generated.
  
  if (!Builder->BuildSinks && Dst.size() == size && !Builder->HasGeneratedNode)
    MakeNode(Dst, S, Pred, GetState(Pred));
}

void GRExprEngine::VisitReturnStmt(ReturnStmt* S, NodeTy* Pred, NodeSet& Dst) {

  Expr* R = S->getRetValue();
  
  if (!R) {
    EvalReturn(Dst, S, Pred);
    return;
  }

  NodeSet DstRet;
  QualType T = R->getType();
  
  if (T->isPointerLikeType()) {
    
    // Check if any of the return values return the address of a stack variable.
    
    NodeSet Tmp;
    Visit(R, Pred, Tmp);
    
    for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {
      RVal X = GetRVal((*I)->getState(), R);

      if (isa<lval::DeclVal>(X)) {
        
        if (cast<lval::DeclVal>(X).getDecl()->hasLocalStorage()) {
        
          // Create a special node representing the v
          
          NodeTy* RetStackNode = Builder->generateNode(S, GetState(*I), *I);
          
          if (RetStackNode) {
            RetStackNode->markAsSink();
            RetsStackAddr.insert(RetStackNode);
          }
          
          continue;
        }
      }
      
      DstRet.Add(*I);
    }
  }
  else
    Visit(R, Pred, DstRet);
  
  for (NodeSet::iterator I=DstRet.begin(), E=DstRet.end(); I!=E; ++I)
    EvalReturn(Dst, S, *I);
}

//===----------------------------------------------------------------------===//
// Transfer functions: Binary operators.
//===----------------------------------------------------------------------===//

bool GRExprEngine::CheckDivideZero(Expr* Ex, ValueState* St,
                                   NodeTy* Pred, RVal Denom) {
  
  // Divide by undefined? (potentially zero)
  
  if (Denom.isUndef()) {
    NodeTy* DivUndef = Builder->generateNode(Ex, St, Pred);
    
    if (DivUndef) {
      DivUndef->markAsSink();
      ExplicitBadDivides.insert(DivUndef);
    }
    
    return true;
  }
  
  // Check for divide/remainder-by-zero.
  // First, "assume" that the denominator is 0 or undefined.            
  
  bool isFeasibleZero = false;
  ValueState* ZeroSt =  Assume(St, Denom, false, isFeasibleZero);
  
  // Second, "assume" that the denominator cannot be 0.            
  
  bool isFeasibleNotZero = false;
  St = Assume(St, Denom, true, isFeasibleNotZero);
  
  // Create the node for the divide-by-zero (if it occurred).
  
  if (isFeasibleZero)
    if (NodeTy* DivZeroNode = Builder->generateNode(Ex, ZeroSt, Pred)) {
      DivZeroNode->markAsSink();
      
      if (isFeasibleNotZero)
        ImplicitBadDivides.insert(DivZeroNode);
      else
        ExplicitBadDivides.insert(DivZeroNode);
      
    }
  
  return !isFeasibleNotZero;
}

void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
                                       GRExprEngine::NodeTy* Pred,
                                       GRExprEngine::NodeSet& Dst) {

  NodeSet Tmp1;
  Expr* LHS = B->getLHS()->IgnoreParens();
  Expr* RHS = B->getRHS()->IgnoreParens();
  
  if (B->isAssignmentOp())
    VisitLVal(LHS, Pred, Tmp1);
  else
    Visit(LHS, Pred, Tmp1);

  for (NodeSet::iterator I1=Tmp1.begin(), E1=Tmp1.end(); I1 != E1; ++I1) {

    RVal LeftV = GetRVal((*I1)->getState(), LHS);
    
    // Process the RHS.
    
    NodeSet Tmp2;
    Visit(RHS, *I1, Tmp2);
    
    // With both the LHS and RHS evaluated, process the operation itself.
    
    for (NodeSet::iterator I2=Tmp2.begin(), E2=Tmp2.end(); I2 != E2; ++I2) {

      ValueState* St = GetState(*I2);
      RVal RightV = GetRVal(St, RHS);
      BinaryOperator::Opcode Op = B->getOpcode();
      
      switch (Op) {
          
        case BinaryOperator::Assign: {
          
          // EXPERIMENTAL: "Conjured" symbols.
          
          if (RightV.isUnknown()) {            
            unsigned Count = Builder->getCurrentBlockCount();
            SymbolID Sym = SymMgr.getConjuredSymbol(B->getRHS(), Count);
            
            RightV = IsPointerType(B->getRHS()->getType()) 
                   ? cast<RVal>(lval::SymbolVal(Sym)) 
                   : cast<RVal>(nonlval::SymbolVal(Sym));            
          }
          
          // Simulate the effects of a "store":  bind the value of the RHS
          // to the L-Value represented by the LHS.
          
          EvalStore(Dst, B, *I2, SetRVal(St, B, RightV), LeftV, RightV);          
          continue;
        }
          
        case BinaryOperator::Div:
        case BinaryOperator::Rem:
          
          // Special checking for integer denominators.
          
          if (RHS->getType()->isIntegerType()
              && CheckDivideZero(B, St, *I2, RightV))
            continue;
          
          // FALL-THROUGH.

        default: {
      
          if (B->isAssignmentOp())
            break;
          
          // Process non-assignements except commas or short-circuited
          // logical expressions (LAnd and LOr).
          
          RVal Result = EvalBinOp(Op, LeftV, RightV);
          
          if (Result.isUnknown()) {
            Dst.Add(*I2);
            continue;
          }
          
          if (Result.isUndef() && !LeftV.isUndef() && !RightV.isUndef()) {
            
            // The operands were *not* undefined, but the result is undefined.
            // This is a special node that should be flagged as an error.
            
            if (NodeTy* UndefNode = Builder->generateNode(B, St, *I2)) {
              UndefNode->markAsSink();            
              UndefResults.insert(UndefNode);
            }
            
            continue;
          }
          
          // Otherwise, create a new node.
          
          MakeNode(Dst, B, *I2, SetRVal(St, B, Result));
          continue;
        }
      }
    
      assert (B->isCompoundAssignmentOp());

      if (Op >= BinaryOperator::AndAssign)
        ((int&) Op) -= (BinaryOperator::AndAssign - BinaryOperator::And);
      else
        ((int&) Op) -= BinaryOperator::MulAssign;  
          
      // Perform a load (the LHS).  This performs the checks for
      // null dereferences, and so on.
      NodeSet Tmp3;
      RVal location = GetRVal(St, LHS);
      EvalLoad(Tmp3, LHS, *I2, St, location);
      
      for (NodeSet::iterator I3=Tmp3.begin(), E3=Tmp3.end(); I3!=E3; ++I3) {
        
        St = GetState(*I3);
        RVal V = GetRVal(St, LHS);

        // Propagate undefined values (left-side).          
        if (V.isUndef()) {
          EvalStore(Dst, B, *I3, SetRVal(St, B, V), location, V);
          continue;
        }
        
        // Propagate unknown values (left and right-side).
        if (RightV.isUnknown() || V.isUnknown()) {
          EvalStore(Dst, B, *I3, SetRVal(St, B, UnknownVal()), location,
                    UnknownVal());
          continue;
        }

        // At this point:
        //
        //  The LHS is not Undef/Unknown.
        //  The RHS is not Unknown.
        
        // Get the computation type.
        QualType CTy = cast<CompoundAssignOperator>(B)->getComputationType();
          
        // Perform promotions.
        V = EvalCast(V, CTy);
        RightV = EvalCast(RightV, CTy);
          
        // Evaluate operands and promote to result type.                    

        if ((Op == BinaryOperator::Div || Op == BinaryOperator::Rem)
             && RHS->getType()->isIntegerType()) {
          
          if (CheckDivideZero(B, St, *I3, RightV))
            continue;
        }
        else if (RightV.isUndef()) {
            
          // Propagate undefined values (right-side).
          
          EvalStore(Dst, B, *I3, SetRVal(St, B, RightV), location, RightV);
          continue;
        }
      
        // Compute the result of the operation.
      
        RVal Result = EvalCast(EvalBinOp(Op, V, RightV), B->getType());
          
        if (Result.isUndef()) {
            
          // The operands were not undefined, but the result is undefined.
          
          if (NodeTy* UndefNode = Builder->generateNode(B, St, *I3)) {
            UndefNode->markAsSink();            
            UndefResults.insert(UndefNode);
          }
          
          continue;
        }
 
        EvalStore(Dst, B, *I3, SetRVal(St, B, Result), location, Result);
      }
    }
  }
}

//===----------------------------------------------------------------------===//
// "Assume" logic.
//===----------------------------------------------------------------------===//

ValueState* GRExprEngine::Assume(ValueState* St, LVal Cond,
                                 bool Assumption, bool& isFeasible) {
                                             
  St = AssumeAux(St, Cond, Assumption, isFeasible);
  
  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
                    : St;
}