Search code examples
cframa-c

Is it possible to specify a buffer access clause in frama-c?

Assuming I have the following function:

void process_data(uint32_t * data, size_t length) {
    for (size_t i = 0; i < length; i++) {
        foo(data[i]);
    }
}

How can I tell Frama-C “this function ensures every access to data[i] satisfies condition i < length”? As far as I understand, I can place an assertion near every line of code that reads data, but is there a better way?

Solution

  • To prevent invalid memory accesses, you need to check that this function is always called with a data pointer from which at least length elements can be read. So you need to write a precondition:

    //@ requires \valid_read (data + (0 .. length-1));
void process_data(uint32_t * data, size_t length) {

    So if you can ensure that this property is valid, it guarantees that you won't have any invalid memory accesses.