--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on March 2015 ---
Thank you for your answer. Does Frama-C release bug patches time to time? Or, is it updated once a year? I'd like to know when the bug is going to be fixed. Thanks, Junkil On Mon, Mar 30, 2015 at 5:05 AM, Lo?c Correnson <loic.correnson at cea.fr> wrote: > Yes, this is a bug indeed. > You can turn around with -wp-no-let. > L. > > > Le 30 mars 2015 ? 03:06, Junkil (David) Park <junkil.park at cis.upenn.edu> > a ?crit : > > > > Hi, > > > > There seems to be something wrong with Frama-C/WP (Sodium) with 5 or > more existential variables in the specification. > > > > // dummy.c > > void dummy() > > { > > double d = 7; > > //@ assert \exists real r1, r2, r3, r4, r5; d == r1 + r2 + r3 + r4 > + r5; > > } > > > > > frama-c -wp dummy.c > > [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no > preprocessing) > > [kernel] Parsing dummy.c (with preprocessing) > > [wp] Running WP plugin... > > [wp] Collecting axiomatic usage > > [wp] warning: Missing RTE guards > > [wp] 1 goal scheduled > > [wp] Proved goals: 0 / 1 > > > > In the example above, Frama-C/WP doesn't try to prove it. > > > > In addition, for the command below, it generate nothing. > > > frama-c -wp -wp-prover why3 -wp-gen -wp-out dummy dummy.c > > > > With 4 existential variables instead of 5, Frama-C/WP works fine. > > > > > > Am I missing something? Or, is it an issue of the new version of Frama-C? > > > > Thanks, > > Junkil > > _______________________________________________ > > 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 > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150331/d73fefed/attachment.html>