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