--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2014 ---
Hi there. My students were quite happy when they succeeded in proving with Frama-C that one of their programs satisfied the contract they believed was the right one. However, they discovered that Frama-C proves the ensures clause also with a too-weak requires clause that, because of unsigned overflows, makes the contract false for (at least) one input value. The program is attached: it was analyzed with Neon on a 64-bit Ubuntu 14.04 machine. We used Alt-Ergo and we have both "RTE" and "Invariants" selected. All the balls apart from the one on the requires clause come out green. On the "Console" tab we have: [kernel] preprocessing with "gcc -C -E -I. sum.c" [rte] annotating function sum [wp] Collecting axiomatic usage sum.c:15:[wp] warning: Missing assigns clause (assigns 'everything' instead) [wp] 7 goals scheduled [wp] Proved goals: 0 / 7 [wp] [Qed] Goal typed_sum_assert_rte_unsigned_overflow : Valid (1ms) [wp] [Qed] Goal typed_sum_assert_rte_unsigned_overflow_3 : Valid (1ms) [wp] [Alt-Ergo] Goal typed_sum_assert_rte_unsigned_overflow_2 : Valid (Qed:1ms) (27ms) (5) [wp] [Alt-Ergo] Goal typed_sum_post : Valid (Qed:3ms) (86ms) (19) [wp] [Qed] Goal typed_sum_loop_term_positive : Valid [wp] [Alt-Ergo] Goal typed_sum_loop_term_decrease : Valid (22ms) (10) [wp] [Alt-Ergo] Goal typed_sum_inv : Valid (Qed:1ms) (910ms) (8) We are puzzled: what are we missing? Kind regards, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara at cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara at bugseng.com -------------- next part -------------- #include <assert.h> /* requires n <= 92681; ensures \result == (n*(n + 1))/2; */ /*@ requires n <= 92682; ensures \result == (n*(n + 1))/2; */ unsigned int sum(unsigned int n) { unsigned int ris; /*@ loop variant n; */ for (ris = 0U; n > 0U; --n) { /* This assertion would fail: assert((((unsigned long long)ris) + n) > 4294967295ULL); */ ris += n; /*@ invariant ris+(n*(n-1)/2) == \at(n,Pre)*(\at(n,Pre)+1)/2; */ } return ris; } int main() { unsigned int n = 92682U; unsigned int r = sum(n); unsigned long long rl = r; unsigned long long nl = n; assert(rl == (nl*(nl + 1))/2); return 0; }