Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Thu, 17 Oct 2013 09:21:25 +0200
  • In-reply-to: <CAC3Lx=aQtcuE8VQXU-eBTS1Gcj3+F-9y_msTUFrArAZ7Ne2E2g@mail.gmail.com>
  • References: <CAP6nMJSdSknD8vZDppXi0aNz55zmyi_98ajThBmcMOn3Buks7Q@mail.gmail.com> <CAC3Lx=aQtcuE8VQXU-eBTS1Gcj3+F-9y_msTUFrArAZ7Ne2E2g@mail.gmail.com>

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                    |