--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assignments proof



Hello,

2013/9/3 David MENTRE <dmentre at linux-france.org>:
> 2013/9/3 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
>> We are using the Carbon version.
>
> Your Inic2 contract is fully proved by WP with Frama-C Fluorine (June)
> and Alt-Ergo 0.95.1. You'd better upgrade your Frama-C version.
>

It'd be indeed a good idea to upgrade, as Carbon is showing its age,
but be careful that by default WP computes on reals (see WP manual,
section 1.5). With the following command line:

frama-c -wp -pp-annot float.c -wp-model +float

alt-ergo does not prove any ensures. On the other hand, with

frama-c -wp -pp-annot float.c -wp-model +float -wp-proof why3:gappa

gappa succeeds in discharging all 3 ensures.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile