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

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