[cfe-commits] [patch] Tracking simple arithmetic constraints (PR2695)

[Ted Kremenek]

Hi Jordy,

I am combing through the patch.  I had a quick question.  Regarding:

const GRState*
RangeConstraintManager::AssumeSymLT(const GRState* state, SymbolRef sym,
                                    const llvm::APSInt& Int,
                                    const llvm::APSInt& Adjustment) {
  ...
  // Special case for Int == Min. This is always false.
  if (Int == Min)
    return NULL;

  llvm::APSInt Lower = Min-Adjustment;
  llvm::APSInt Upper = Int-Adjustment;


Are you assuming that APSInt handles overflow semantics here?  Specifically, can't 'Min - Adjustment' overflow?  Same with 'Int - Adjustment'.

On Jun 14, 2010, at 1:21 PM, Jordy Rose wrote:

> Finally revised and with better test cases.
> 
> Summary of changes:
> - SimpleSValuator folds additive expressions ("$sym + k1 - k2").
> 
> - SimpleSValuator does not make UnknownVals everywhere it could. When the
> LHS is a symbol or symbolic expression, it should probably only make a
> SymExprVal if the constraint manager actually canReasonAbout() it.
> 
> - SimpleConstraintManager's subclasses can now handle expressions of the
> form "($sym + k1) <> k2", where "<>" is a comparison operator.
> 
> - SimpleConstraintManager's AssumeSymREL (pure virtual) methods take an
> extra "adjustment" parameter. This corresponds to "k1" in the above
> expression.
> 
> - RangeSets (an implementation detail of RangeConstraintManager) are now
> narrowed down using "intersections", rather than comparison-based
> constraints.
> 
> - Overflow is modeled for both unsigned and signed types.
> 
> - There is no special testing for true tautological expressions (x + k1 <
> MAX).
> 
> - There is now a static version of BinaryOperator::isAdditiveOp().<additive-folding.patch>