Hi all,

Hi guys,

I’m investigating the constraints being dropped, here’s what I got so far.

First of all, I’m using the following program:

void foo(unsigned width)

{

int base;

int i = 0;

if (!(i % width))

base = 1;

if(base == 1)

abort();

}

I started by looking at ExprEngine::processBranch, where

SVal X = PrevState->getSVal(Condition, PredI->getLocationContext());

returns Unknown for the remainder condition. The getSVal ends up looking in a map for the value result, so I found that bindExpr fills that map.

Going back a bit, into ExprEngine::Visit, when evaluating a Stmt::BinaryOperatorClass (regardless of the eagerly assume flag) ExprEngine::VisitBinaryOperator is called, which eventually calls evalBinOp and, since it doesn’t understand remainder, it returns unknown and BindExpr is never called.

Back to ExprEngine::processBranch, when the symbol is unknown the following piece of code is called:

// If the condition is still unknown, give up.

if (X.isUnknownOrUndef()) {

builder.generateNode(PrevState, true, PredI);

builder.generateNode(PrevState, false, PredI);

continue;

}

and the condition is simply ignored. When the result is defined, it creates two nodes assuming the constraints.