--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2014 ---
Hi, Thanks for the report. It looks like a bug in proof obligations with -wp-invariants for the RTE assertions. Reformulating the code with a loop invariant (instead of generalized invariant) highlights the problem: there is a potential overflow for large values of n. Or, perhaps a 64bit architecture is necessary (use -machdep help). Moreover, Alt-Ergo requires an additional lemma to convert n(n+1)/2 into n(n-1)/2+n ; This lemma can be proved with Coq (or left unproved), see attached files. However, it is surprising that value-analysis plugin does not complain for this potential overflow. To reproduce : # frama-c sum.i -wp -wp-rte -wp-script sum.s -wp-prover alt-ergo,coq # frama-c sum.i -val -main sum (see attached files sum.s and sum.i) As a final remark, you should use the following prototype for 'assert' instead of the standard one: //@ ensures a ; exits !a ; assigns \nothing ; void assert(int a); ________________________________________ De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Roberto Bagnara [bagnara at cs.unipr.it] Envoy? : mardi 20 mai 2014 11:43 ? : Frama-C public discussion Objet : [Frama-c-discuss] Puzzled about apparent proof of false contract 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 -------------- A non-text attachment was scrubbed... Name: sum.s Type: application/octet-stream Size: 654 bytes Desc: sum.s URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140520/55feb0b9/attachment.obj> -------------- next part -------------- A non-text attachment was scrubbed... Name: sum.i Type: application/octet-stream Size: 362 bytes Desc: sum.i URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140520/55feb0b9/attachment-0001.obj>