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