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