# 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] Puzzled about apparent proof of false contract

*Subject*: [Frama-c-discuss] Puzzled about apparent proof of false contract*From*: loic.correnson at cea.fr (CORRENSON Loic 218851)*Date*: Tue, 20 May 2014 13:48:55 +0000*In-reply-to*: <537B23C4.9010700@cs.unipr.it>*References*: <537B23C4.9010700@cs.unipr.it>

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>

**Follow-Ups**:**[Frama-c-discuss] Puzzled about apparent proof of false contract***From:*virgile.prevosto at m4x.org (Virgile Prevosto)

**References**:**[Frama-c-discuss] Puzzled about apparent proof of false contract***From:*bagnara at cs.unipr.it (Roberto Bagnara)

- Prev by Date:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Next by Date:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Previous by thread:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Next by thread:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Index(es):