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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Tue, 1 Sep 2015 12:47:44 +0200
  • In-reply-to: <CAL+X0ekn0=s=cL-1qKn8tVrAa44wJvfvf64CUeF=Nhbu2WZC5g@mail.gmail.com>
  • References: <CAL+X0em51tXgG9rdDtG3w6O3x+7Zxvp1Q0cQt_Pc_fi_bs=cAA@mail.gmail.com> <55E3EBE7.8000806@cea.fr> <CAL+X0ekn0=s=cL-1qKn8tVrAa44wJvfvf64CUeF=Nhbu2WZC5g@mail.gmail.com>
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>