search

xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
173 stars 4 forks source link

buffer overflows planning #55

Closed claude-betz closed 2 months ago

claude-betz commented 3 months ago

Following our roadmap this is next up.

We currently don't track the sizes of objects within our model of C's semantics. This means means we don't detect the overflow in situations such as.

void
foo()
{
    int *p;
    p = malloc(sizeof(int) * 2); 
    p[2] = 1;
}