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] Speedup Frama-C/WP generating proof obligations
- Subject: [Frama-c-discuss] Speedup Frama-C/WP generating proof obligations
- From: junkil.park at cis.upenn.edu (Junkil (David) Park)
- Date: Thu, 27 Aug 2015 14:53:44 -0400
Hi, I have 5000 lines of C code with one assertion to prove. Since I'd like to generate the proof obligations of it in Why3, I typed the command-line as follows: > frama-c -wp -wp-prover why3 -wp-gen -wp-out out_dir code.c It takes about 50 seconds to complete finishing the generation. However, I'd like to speed up if possible because I need to do it repeatedly even with longer C code. When I typed the command-line above, Frama-C/WP displays "[wp] 2 goals scheduled" in 30 seconds. After that, it terminates displaying "[wp] Proved goals: 0 / 2" in another 20 seconds. I wonder if Frama-C/WP internally makes any attempts to prove those goals. I wonder if I set an option flag for Frama-C not to try to prove them, but just to generate the proof obligations. I tried to turn off the Qed Simplifier's options (-wp-no-simpl, -wp-no-clean, ...), but it didn't help reducing the running time of Frama-C. Are there be any other options that can help reducing the time of generating the proof obligations only? Thanks, Junkil -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150827/68b076a5/attachment.html>
- Follow-Ups:
- [Frama-c-discuss] Speedup Frama-C/WP generating proof obligations
- From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
- [Frama-c-discuss] Speedup Frama-C/WP generating proof obligations
- Prev by Date: [Frama-c-discuss] my first frama verification
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] headers question
- Next by thread: [Frama-c-discuss] Speedup Frama-C/WP generating proof obligations
- Index(es):