--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on August 2015 ---
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>