--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2014 ---
[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>