--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Speedup Frama-C/WP generating proof obligations



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>