False positive out of bounds (C)

symbolic_execution
cpp

(Richard Robbins) #1

Link to bug report in project

I haven’t tried a minimal test case in practice, but unless I’m missing something, I believe the code can be reduced to:

#define MAX_SEARCH 10

char buf[MAX_SEARCH];
size_t buf_i;

void
foo(char c)
{
    if (buf_i < (sizeof(buf) - 1)) {
        buf[buf_i++] = c;
        buf[buf_i] = 0;
    }
}

If buf_i is strictly less than (sizeof(buf) - 1)) we have
buf_i < (10 - 1)
buf_i is at most 8.
In which case both accesses to
buf[8]
buf[9]
are valid, though the later is being reported as out of bounds.


(Loïc Joly) #2

Hello Richard,

You are right this is a bug, and I’ve been able to reproduce it with your sample, and to reduce it even further:

char buf[10];
unsigned long long buf_i;

void foo() {
    if (buf_i < 5) {
        buf[buf_i+1] = 0;
    }
}

It seems that the problem generates false-positives on a limited number of case. In the above example, no false-positive are raised for “unsigned long” for example.
This is a good finding, thanks for having raised our attention on it.

There is sadly no easy quick fix I can do so for the moment there is no any ETA to solve this problem. Until we managed to find a solution, I recommend you to flag this issue as false-positive.