--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] existential variables in ACSL spec in Frama-C/WP Sodium



It?s depend on your needs. We produce one or two releases a year.
You can also subscribe to commercial support to benefit from dedicated support for bug-fixing and small feature development.
Regards,
L.

> Le 31 mars 2015 ? 19:57, Junkil (David) Park <junkil.park at cis.upenn.edu> a ?crit :
> 
> 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 <mailto: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 <mailto: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 <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <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 <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <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/20150401/c489e8de/attachment.html>