--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Array problem - Jessie plugin



Hi Claude,


Thank you for your answer. It has worked.

Best regards.

Luciana






2013/10/25 Claude Marche <Claude.Marche at inria.fr>

>
> Hi,
>
> This is the same situation as your example with a struct. The workaround
> is to introduce a ghost variable.
>
> There is no need to introduce ghost variables when you have two or more
> array assignments because Jessie does a special treatment of parallel
> assignments. However, the current discussion make me think that every
> assignments should be treated as parallel assignments are treated. I may
> consider adding this in the next release.
>
> - Claude
>
> On 10/21/2013 02:03 PM, Luciana Burgareli wrote:
> > Hi,
> >
> > This is a very simple example, but it was not proved.
> >
> > If we slightly modify the code and we add an assignment to the Ang2[1]
> > (and the related assigns and ensures clauses), both the ensures clauses
> > are proved.
> >
> > Why is not the attached example proved?
> >
> > How to solve this problem?
> >
> > We are using the Jessie Plugin, Why3 Verification Platform 0.81,
> > Fluorine-20130601 and the provers Alt-Ergo 0.95.2, CVC3 2.4.1, Gappa
> > 1.0.0 and Z3 4.3.2.
> >
> >
> > Luciana
> >
> >
> >
> > _______________________________________________
> > 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/20131031/cc1822b8/attachment.html>