--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on October 2013 ---
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>