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>