--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on October 2013 ---
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>