[cfe-dev] Need info about ProgramState, SymbolReaper, etc

[Daniel Marjamäki]

Hello Ted!

Thanks for your response.

> The ProgramState doesn’t need to track the value ‘7’ because that’s easily recoverable lazily.

I am afraid I am confused.

I don't really care about RHS. If I need to track '7' somehow.. then I don't understand why.

To clarify.. the ProgramState is used to track variables.. right?

When I dump ProgramState I can get such output:

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] }

This output above means that the variable 'x' currently has the min value 20 .. right? I hope that is what it means.

The ArrayBoundsChecker uses ProgramState to determine if a variable, for example 'x', is out of bounds ... right?

The ArrayBoundsChecker does not have fundamental problems with 'a[x] = 7'. For example:

void f(int x) {
    int a[10];
    if (x == 20)
        a[x] = 7;
}

The output is:
a.c:5:14: warning: Access out-of-bound array element (buffer overflow)
        a[x] = 7;
        ~~~~ ^

This is good.

But then, when I change the '==' to '>=' then no warning is reported. 

void f(int x) {
    int a[10];
    if (x >= 20)
        a[x] = 7;
}

I have the feeling that you have trouble reproducing.

I use this command line:
clang -cc1 -analyze -analyzer-checker=alpha,core a.c

If I need to use some other flags then please let me know.

> When you say “there is a warning”, are you using an unmodified ArrayBoundChecker, or does this involve new logic you have written?

This happens both with the latest release (I've installed the official windows binaries) and with svn top (compiled by myself, both in windows and linux).

Best regards,
Daniel Marjamäki