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: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Mon, 31 Aug 2015 07:53:43 +0200
  • In-reply-to: <CAL+X0em51tXgG9rdDtG3w6O3x+7Zxvp1Q0cQt_Pc_fi_bs=cAA@mail.gmail.com>
  • References: <CAL+X0em51tXgG9rdDtG3w6O3x+7Zxvp1Q0cQt_Pc_fi_bs=cAA@mail.gmail.com>
Le 27/08/2015 20:53, Junkil (David) Park a écrit :
> 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.
The option "-wp-proof none" skips the file generation for external provers.
>
> 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?
>
Sorry, Qed Simplifier cannot be turned off completly.
> Thanks,
> Junkil

Patrick.

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150831/5d73f43f/attachment.html>