--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on October 2013 ---
Hello Nanci, 2013/10/16 Nanci Naomi <nnarai at gmail.com>: > 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? Because you have you have a _sequence_ of independent "if". After the first if, you have 2 sets of VCs (first if taken or not), after the second if, 4 sets of VCs (first if taken and second if not taken, first if taken and second if taken, ...), 8 sets after the 3rd if, and so on with exponential growth. > How to verify this code in a reasonable time? 1. Change the code structure to use "else if" instead of if. This might not be always possible (legacy code that must not change for example); 2. Change the weakest precondition generation algorithm (see below); 3. Buy/rent a faster machine. > 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? There are algorithms changing the way VC are generated, generating less numerous but at the same time more complicated VCs. Why2 has this algorithm. Why3 should have it now (at least in the latest development branch). Now I don't know if -jessie-why-opt="-fast-wp" should activate this algorithm or not in your configuration. I let experts respond to this part. Best regards, david