--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on October 2013 ---
Le 17/10/2013 08:27, David MENTRE a ?crit : > 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. This is too optimistic: tests of the form if (c1 && c2) { i }; generate not 2 but 3 branch in the control flow, because if the lazy evaluation of &&. Since you have 7 such piece of code in sequence, you have 3^7 branches, a bit more than 2,000, explaining the 2,000 VCs >> 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? this option works only if you use Why2 VCgen and not Why3. > 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. There is on-going development of a fast-wp algorithm in Why3, but not yet available. > Best regards, > david > > _______________________________________________ > 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 |