Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RTE array index bounds

  • Subject: [Frama-c-discuss] RTE array index bounds
  • From: mansourmoufid at gmail.com (Mansour Moufid)
  • Date: Mon, 6 Oct 2014 23:26:56 -0400
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