--- layout: fc_discuss_archives title: Message 66 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



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>