Hello!

I am trying to figure out how to make clang warn for this code:

void f(int x) {

int a[10];

if (x >= 20)

a[x] = 7;

}

If the "7" is replaced with "x" then there is a warning.

As far as I see, ArrayBoundChecker works as it should. I believe the problem is related with the ProgramState.

The ProgramState when ArrayBoundChecker::checkLocation is called for 'a[x] = x':

Expressions:

(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}

(0x5c2f900,0x5bdb4c8) x : reg_$0<x>

(0x5c2f900,0x5c24930) a[x] = x : reg_$0<x>

Ranges of symbol values:

reg_$0<x> : { [20, 2147483647] }

The ProgramState when ArrayBoundChecker::checkLocation is called for 'a[x] = 7':

Expressions:

(0x5c2f900,0x5bdb340) x : &x

(0x5c2f900,0x5bdb388) x : reg_$0<x>

Ranges are empty.

I believe the "Ranges are empty" message is a problem. I have tried to track down why the ranges are empty. The ranges is removed somehow in the function ProgramStateManager::removeDeadBindings(). I don't understand why "7" will make the ranges empty and "x" will not.. but I assume that the bug is not located in this function but somehow somewhere else (earlier?).

In ProgramStateManager::removeDeadBindings(), the ProgramState will initially be:

Expressions:

(0x5c2f900,0x5bdb3c8) a : &a

(0x5c2f900,0x5bdb3f0) x : &x

(0x5c2f900,0x5bdb448) a : &element{a,0 S32b,int}

(0x5c2f900,0x5bdb460) x : reg_$0<x>

(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}

Ranges of symbol values:

reg_$0<x> : { [20, 2147483647] }

After this statement:

ProgramStateRef Result = getPersistentState(NewState);

The 'Result' is:

Expressions:

(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}

Ranges of symbol values:

reg_$0<x> : { [20, 2147483647] }

The next statement is:

return ConstraintMgr->removeDeadBindings(Result, SymReaper);

Here the ranges are removed.

Do you think I am on the right track? I feel that I need some help to get further. I can't solve this on my own. Could anybody tell me how I should proceed.

Best regards,

Daniel Marjamäki

..................................................................................................................

Daniel Marjamäki Senior Engineer

Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden

Mobile: +46 (0)709 12 42 62

E-mail: Daniel.Marjamaki@evidente.se

www.evidente.se