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

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



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>