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: junkil.park at cis.upenn.edu (Junkil (David) Park)
  • Date: Mon, 31 Aug 2015 10:08:33 -0400
  • In-reply-to: <55E3EBE7.8000806@cea.fr>
  • References: <CAL+X0em51tXgG9rdDtG3w6O3x+7Zxvp1Q0cQt_Pc_fi_bs=cAA@mail.gmail.com> <55E3EBE7.8000806@cea.fr>
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>