--- layout: fc_discuss_archives title: Message 63 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



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