xr0-org / xr0

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

buffer overflows: general case #60

Open akiarie opened 2 months ago

akiarie commented 2 months ago

This seems sufficiently expressed in

int
zeroindex(int *arr, int index)
{
        arr[index] = 0;
}

We can use an abstract like

int
zeroindex(int *arr, int index) ~ [
        setup: arr = .clump(sizeof(int)) - index;
        arr[index] = 0;
];

A more complex example is as follows:

zeroall(int *arr, int len) ~ [
        int i;
        setup: arr = .clump(sizeof(int)*len);
        for (i = 0; i < len; i++) {
                arr[i] = 0;
        }
]{
        int i;
        for (i = 0; i < len; i++) {
                arr[i] = 0;
        }
}