--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RTE array index bounds



Hi everyone,

I would like to prove that indices to access an array are bounded
properly, using the WPE plugin, after reading data into the array.

For example, in this program:

    #include <stdio.h>
    #include <unistd.h>
    int main(void)
    {
        char buffer[10];
        ssize_t i;
        size_t j;
        i = read(0, buffer, sizeof(buffer));
        if (i <= 0) {
            return 1;
        }
        for (j = 0; j < (size_t) i; j++) {
            if (buffer[j] == '\n') {
                buffer[j] = '\0';
                break;
            }
        }
        puts(buffer);
        return 0;
    }

the variable j should be bounded by [0, sizeof(buffer)].

But it seems only the lower bound is proven:

    $ frama-c -pp-annot -wp -wp-rte bar.c
    ...
    [wp] [Qed] Goal typed_main_assert_rte_index_bound_2 : Valid
    [wp] [Alt-Ergo] Goal typed_main_assert_rte_index_bound : Unknown
    (Qed:4ms)

I think the WPE plugin doesn't know that the return value of the read
function is always less than or equal to its third argument, so I add
the following annotation above the main function:

    /*@ ensures \result <= nbyte; */
    ssize_t read(int fildes, void *buf, size_t nbyte);

but it doesn't help:

    Goal Assertion 'rte,index_bound' (file bar.c, line 20):
    Let a_0 = (global L_buffer_1658).
    ...
    Prove: j_4<=9.
    Prover Alt-Ergo returns Unknown (Qed:4ms) (1s)

How can I prove the index bounds in this case? I would appreciate
any help.

Mansour