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,

2013/10/17 Nanci Naomi <nnarai at gmail.com>:
>> 3. Buy/rent a faster machine.
>
>
> our machine is a Mac Boo Pro, processor: 2.9 GHz Intel Core i7, memory: 8
> GB.
> this example with about 2,000 VCs is verified in about 10 minutes, but our
> original source code with 6,000 VCs is analyzed very slowly, the Alt-ergo
> prover takes about 24 hours without finishing the analysis.

Probably the main issue is that each time you make a modification, you
need to redo *all* the VCs. Not very usable in practice.

GNATprove (technology similar to Frama-C but applied on Ada) provides
a cache mechanism that avoids re-doing VCs that haven't changed. Maybe
a future improvement for Frama-C?


> then, we replaced the suggested annotation by this one:
>  /*@ assigns flag;
>   @ ensures (a && !a1) ==> flag == time1;
>   @ ensures !(a && !a1) ==> \old(flag);
>   @*/
>  if(a == TRUE && a1 == FALSE)
>  {
>   flag = time1;
>  }
>
> it ran, but how do this work?
> Sorry, but I did not understand how these annotations will make possible to
> run the analysis in a shorter time.

[Claude will probably correct me. ;-) ] This annotation substitutes,
within the logical framework of Jessie, the "if" piece of code by the
given assertion which is equal to one (or two?) logical formula (((a
&& !a1) ==> flag == time1) && ( !(a && !a1) ==> \old(flag))). Then,
when the weakest precondition generation algorithm is applied, this
unique logical formula is used instead of the 3 logical formulas
generated from the "if" construct, thus the reduction on the number of
VCs.

You would obtain the same result by putting part of your code into
another function, with a proper contract to represent the
corresponding code and call it from the original function. Which
brings me to a fourth proposal:

 4. Cut the original code into several sub functions, with for each
called function a contract summarizing the corresponding code.

I know this approach is sometimes used into other formalisms, for
example using LOCAL_OPERATIONS in B Method.

Best regards,
david