--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on August 2015 ---
Hi Patrick, Thank you for your answer. Sorry, Qed Simplifier cannot be turned off completely. Is there a way for me to measure the running time of Qed Simplifier (or, the running time of each component of Qed Simplifier if possible)? Is there any other options that I can control for the behavior of Qed Simplifier? It is because I am trying to verify hundreds of C code using the Frama-C/WPâWhy3--Z3 tool chain. Some C code are 5,000 lines long, some are 30,000 lines long, some are longer. In the toolchain, I currently experience that the bottleneck is Frama-C/WP. For one case, while Frama-C/WP takes 900 seconds, Why3âZ3 take less than 1 second. If Iâm right, I think that the Qed Simplifier is related to the reasons why Frama-C/WP is slow. So, Iâd like to have more control of the behavior of Qed, and do a test. Thanks, Junkil On Mon, Aug 31, 2015 at 1:53 AM, BAUDIN Patrick <Patrick.Baudin at cea.fr> wrote: > 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. > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150831/75a37c54/attachment.html>