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

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>