--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on October 2013 ---
Now, what is the work-around? A solution, that does not need to change the code, is to annotate the if instructions with code contracts, for example: /*@ assigns x; @ ensures x == (c1 && c2) ? e : \old(x); @*/ if (c1 && c2) { x = e } (assuming c1,c2 and e have no side-effects) - Claude Le 16/10/2013 21:44, Nanci Naomi a ?crit : > 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) > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |