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: nnarai at gmail.com (Nanci Naomi)
  • Date: Thu, 17 Oct 2013 14:30:28 -0300
  • 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>
Thank you very much for all the replies.


> 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);
>

yes, it is a legacy code. Besides that, implementing the "else if" would
change the algorithm.


> 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.

Now, what is the work-around? A solution, that does not need to change
> the code, is to annotate the if instructions with code contracts, for
> example:
>
> /*@ assigns x;
>   @ ensures x == (c1 && c2) ? e : \old(x);
>   @*/
> if (c1 && c2) {
>   x = e
> }
>

we tried this solution, but frama-c shown the following error:
File "test1.jc", line 123, characters 40-123: typing error: numeric or
pointer types expected for == and !=
[jessie] user error: Jessie subprocess failed:   jessie  -why3ml  -v
-locs test1.cloc test1.jc

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.

We would like to report the results from some tests we performed with the
same example. I know that the IF statements generate several branches of
execution, but it does not seem to be the only problem. The same example
without the struct type variable produces only one VC for _Event_Safety.
Thus we could assume the problem is the struct, but I think it is not the
right explanation, because we have other source codes with struct type
variables that generates few VCs.
Would be the result a particular combination of the struct type variable
with the IF statements?

Regards
Nanci
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131017/b00baae6/attachment.html>