--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin - more than 6,000 VCs generated



We have a quite simple algorithm, but its source code generated more than
6,000 VCs.

We have tried to verify the code, but we aborted the verification because
it did not finish after running 24 hours.

We simplified the code a little and are sending you an example with similar
struct type variable and if statements. This example generated more than
2,000 VCs.

Why are generated so many VCs?
How to verify this code in a reasonable time?
We tried to run with the -jessie-why-opt="-fast-wp" option, but it does not
seem to work in the Fluorine version, because the number of VCs did not
decrease.
Is there another option and/or solution?

Nanci Naomi

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Treat the Earth well.  It was not given to you by your parents,
it was loaned to you by your children. (Kenyan proverb)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131016/2af13b35/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test1.c
Type: text/x-csrc
Size: 1190 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131016/2af13b35/attachment.c>