--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2014 ---
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