--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2013 ---
You can use ghost variables to prove correctness of the same code (see attached). Alt+Ergo and Gappa prove correctness of this source. --- Eugene Kornykhin, Lomonosov Moscow State University On 4 October 2013 17:50, Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>wrote: > Hi, > > > The attached source code is a simplified version of the program we are > trying to prove. > Basically, M and L are struct type variables. > > L.M1 is equal to 0.0 and we tried to state this in the requires clause > with the BOUND define. Is it correct? > > We want to prove that M.x1 and result variable are equal to 0.0 too, > but the assert clauses are not proved. What is wrong? > > We are using the Jessie plug-in, 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. > > Best regards, > Nanci, Luciana, Rovedy > > _______________________________________________ > 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/20131008/4142f0ad/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: siteZero.c Type: text/x-csrc Size: 503 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/4142f0ad/attachment.c>