--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated




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                    |