--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on October 2013 ---
On 16/10/2013 21:44, Nanci Naomi wrote: > 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? Hmm... it seems Frama-C options are no longer passed to Why3; that is bad. Manually adding the option "--debug fast_wp" (that is the current name of the fast-wp option) to the why3ide command inside the generated Makefile seems to do the trick. (Except that it will be erased the next time you run Frama-C, I think.) This gets the number of proof obligations after split from 2189 to 2. The fact that there are only two obligations left kind of frightens me, so I cannot guarantee that it works correctly. Best regards, Guillaume