--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on September 2015 ---
Hi, Actually, main costs come from writing down the goals on disk *and* running the provers. In your reports, I understand that most of time is spent in waiting for provers to timeout their goals (10s for each of 2 goals). You must ensure that no prover is actually run ; for Why-3 using `-wp-prover why3ide -wp-gen` should fits your needs. Qed simplification time is printed on stdout if greater than 1ms â and usually, it is *very* small (10-100ms) even on large goals. Still, if Qed appears too much in your cases, you can disable costly simplifications by turning off options in the « Computation Strategy » section of `frama-c -wp-h`, but `-wp-no-simpl` should turn off most of them. However, Iâm a bit surprised by the generation time you mention, which are quite unfamiliar to me, even on large code base. Consider submitting a BTS entry with an example, if you can disclose some. Regards, L. > Le 31 août 2015 à 16:08, Junkil (David) Park <junkil.park at cis.upenn.edu> a écrit : > > 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 <mailto: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 <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss> > > _______________________________________________ > 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/20150901/0caf7733/attachment.html>