--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2014 ---
Thanks for your detailed reply. The behavior spec is not using the "logic max_index..." Is it not supported by WP? Best regards, Dharma From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Cristiano Sousa Sent: Sunday, March 16, 2014 1:08 PM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] WP Question/Bug? Hi, You seem to be missing your loop variant and an invariant indicating how the 'i' variable is bound. You should add: loop invariant -1 <= i < n; loop variant i; With this, the generated memory safety annotations are discharged. However, your post-conditions are not. In situations like this I prefer to annotate each possible outcome of the function using different behaviors. In your case it would look like this: /*@ requires n>=0 && \valid(t+(0..n-1)); assigns \nothing; behavior zero_size: assumes n == 0; ensures \result == 0; behavior no_zero: assumes n > 0; assumes \forall integer j; 0 <= j < n ==> t[j] != 0; ensures \result == 0; behavior has_zero: assumes n > 0; assumes \exists integer j; 0 <= j < n && t[j] == 0; ensures t[\result] == 0; ensures 0 <= \result < n; ensures \forall integer j; j > \result && j < n ==> t[j] != 0; complete behaviors; disjoint behaviors; */ int get_max_index(int t[], int n) { int i = 0; /*@ loop invariant -1 <= i < n; loop invariant \forall integer j; j > i && j < n ==> \at(t[j], Pre) != 0; loop assigns i; loop variant i; */ for(i = n-1; i >=0 ; i--) { if(t[i] == 0) return i; } return 0; } The annotation are longer, but I find it much easier to understand. The above annotations are fully discharged using Frama-C Fluorine 2 and alt-ergo 0.95.1 2014-03-16 16:12 GMT+00:00 Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>>: Hi, I do not understand why the first ensures as well as the generated valid memory access within the loop are not provable. I tried it on the latest version of Frama-c. /*@ logic integer max_index{L}(int* t, integer n) = @ (n==0) ? 0 : @ (t[n-1] == 0) ? n-1 : max_index(t, n-1); */ /*@ requires n>=0 && \valid(t+(0..n-1)); assigns \nothing; ensures \result == max_index(t, n); ensures \forall integer j; j > \result && j < n ==> t[j] != 0; */ int get_max_index(int t[], int n) { int i = 0; /*@ loop invariant \forall integer j; j > i && j < n ==> \at(t[j], Pre) != 0; loop assigns i; */ for(i = n-1; i >=0 ; i--) { if(t[i] == 0) return i; } return 0; } [formal_verification]$ frama-c -wp -wp-rte max_index.c [kernel] preprocessing with "gcc -C -E -I. max_index.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function get_max_index [rte] annotating function main [wp] 14 goals scheduled [wp] [Alt-Ergo] Goal typed_get_max_index_assert_rte_signed_overflow : Valid (8ms) (9) [wp] [Alt-Ergo] Goal typed_get_max_index_loop_inv_preserved : Valid (20ms) (26) [wp] [Alt-Ergo] Goal typed_get_max_index_post_2 : Valid (24ms) (27) [wp] [Qed] Goal typed_get_max_index_loop_inv_established : Valid [wp] [Qed] Goal typed_get_max_index_loop_assign : Valid [wp] [Qed] Goal typed_get_max_index_assign_part1 : Valid (4ms) [wp] [Qed] Goal typed_get_max_index_assign_part2 : Valid [wp] [Alt-Ergo] Goal typed_get_max_index_assert_rte_signed_overflow_2 : Valid (20ms) (16) [wp] [Qed] Goal typed_get_max_index_assign_part3 : Valid [wp] [Alt-Ergo] Goal typed_get_max_index_assert_rte_mem_access : Unknown (1s) [wp] [Qed] Goal typed_get_max_index_assign_part4 : Valid [wp] [Qed] Goal typed_get_max_index_assign_part5 : Valid [wp] [Qed] Goal typed_main_call_get_max_index_pre : Valid [wp] [Alt-Ergo] Goal typed_get_max_index_post : Unknown (Qed:4ms) (6s) [wp] Proved goals: 12 / 14 Qed: 8 (4ms-4ms) Alt-Ergo: 4 (8ms-24ms) (27) (unknown: 2) _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/k-Kr4x8idEICzBwQsL6zBNVUTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK3JgvjpvW_cK9KcTjWZOW8WX7fFCzBWXP7bnhIyyHtBDBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdEI3HzzobZ8Qg6BInzGKBX5Q9kITixFtd402xoQg0eTZ9OH31BIyidIL6_f9Zc-TD> -- Cumprimentos, Cristiano Sousa -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140316/5054ba99/attachment-0001.html>