--- layout: fc_discuss_archives title: Message 10 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



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