Catch buffer overflows in structures

[arthaud]

The current analysis cannot catch a buffer overflow in a structure.

For instance:

#include <ikos/analyzer/intrinsic.h>

typedef struct {
    int tab[10];
    int x;
} Struct;

int main() {
    Struct s;
    s.tab[10] = 1; // overflow on tab, writes on x
    __ikos_assert(s.x == 1);
    return 0;
}

The analyzer only checks that the memory write is within the structure, so it is considered safe.

The analyzer will actually know that s.x is 1, so we could say that the analysis is somewhat sound regarding the memory model.

To fix this, we should investigate the inbounds flag of the LLVM getelementptr instruction.

See:

• LLVM Language Reference Manual
• What happens if an array index is out of bounds?

[ivanperez-keera]

Is this a bug or a feature request?

[ivanperez-keera]

My understanding is that this is not a bug. I'm switching labels accordingly. If you disagree, please revert the change.