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] Jessie plugin - more than 6,000 VCs generated

  • Subject: [Frama-c-discuss] Jessie plugin - more than 6,000 VCs generated
  • From: nnarai at gmail.com (Nanci Naomi)
  • Date: Wed, 16 Oct 2013 16:44:25 -0300
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>