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] WP failing to prove a simple absence of RTE unsigned overflow

Hi,
Option -lib-entry is used in conjunction with -main, as explained in the manual:
In the main function (-main), the global variables have their initial value, unless (-lib-entry) is specified.
L.

Le 4 nov. 2014 ? 10:01, David MENTRE <dmentre at linux-france.org> a ?crit :

> Hello,
> 
> Le 04/11/2014 00:14, Gregory Maxwell a ?crit :
>> frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300
>> -wp-par 1 -wp-rte a.c
> 
> I would invoke Frama-C WP with :
> 
>  frama-c -wp -wp-rte -machdep x86_64 a.c
> 
> -main is not needed, WP takes all given function as input by default.
> 
> I'm not sure -lib-entry is needed, WP doesn't use assumptions on global variables, does it?
> 
> -machdep x86_64 is needed because you are assuming a 64 bits machine.
> 
> With above invocation, 17 of 51 goals are not proved. Using a longer timeout (3s) does not help.
> 
> I tested with Frama-C Neon and Alt-Ergo 0.95.2 (both in opam).
> 
> Best regards,
> david
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss