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

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
}

(assuming c1,c2 and e have no side-effects)

- Claude





Le 16/10/2013 21:44, Nanci Naomi a ?crit :
> 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?
> 
> Nanci Naomi
> 
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Treat the Earth well.  It was not given to you by your parents,
> it was loaned to you by your children. (Kenyan proverb) 
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> 
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |