--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Speedup Frama-C/WP generating proof obligations



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>