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
- Subject: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: dmentre at linux-france.org (David MENTRE)
- Date: Tue, 04 Nov 2014 10:01:55 +0100
- In-reply-to: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>
- References: <CAAS2fgRTEAODJ78tg7m77oDEyK4XG0E0GHLRkrqm7tRNFwY3bg@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- References:
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- From: gmaxwell at gmail.com (Gregory Maxwell)
- [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Prev by Date: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Next by Date: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Previous by thread: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Next by thread: [Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow
- Index(es):