xr0-org / xr0

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

buffer overflows: local-constant size and index #57

Closed akiarie closed 3 days ago

akiarie commented 2 months ago

If the block is defined locally and with compile-constant size, such as in declarations like

int k; int arr[50];

and the pointer is defined with constants also, like

int *p = &k;        /* p[i] valid for i = 0 */

or

int *q = p+5;       /* q[i] valid for i = -5 */

or

int *r = arr+15;    /* r[i] valid for i = -15, ..., 34 */

then it is easy to determine the ranges of valid accessing, as shown in the comments above.