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