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



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                    |