CODEWITHSUNDEEP
cframa-c
Vladislav Ivanov
Vladislav Ivanov

Reputation: 229

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?

Upvotes: 1

Views: 117

Answers (1)

Anne
Anne

Reputation: 1270

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.

Upvotes: 2

Related Questions