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>
_______________________________________________
cfe-commits mailing list
cfe-commits@cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
