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

On 16/10/2013 21:44, Nanci Naomi wrote:
> We have a quite simple algorithm, but its source code generated more
> than 6,000 VCs.
>
> We have tried to verify the code, but we aborted the verification
> because it did not finish after running 24 hours.
>
> 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?
> How to verify this code in a reasonable time?
> 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?

Hmm... it seems Frama-C options are no longer passed to Why3; that is bad.

Manually adding the option "--debug fast_wp" (that is the current name 
of the fast-wp option) to the why3ide command inside the generated 
Makefile seems to do the trick. (Except that it will be erased the next 
time you run Frama-C, I think.)

This gets the number of proof obligations after split from 2189 to 2. 
The fact that there are only two obligations left kind of frightens me, 
so I cannot guarantee that it works correctly.

Best regards,

Guillaume