--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on October 2013 ---
Le 08/10/2013 07:40, Guillaume Melquiond a ?crit : > On 04/10/2013 15:50, Rovedy Aparecida Busquim e Silva wrote: > >> 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? > > I don't see anything wrong with the specification. In fact, if you > replace field M.x1 by some float variable Mx1, it will go through. > >> 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? > > Gappa can prove the arithmetic properties, but it does not support field > accesses. SMT solvers support them, but they cannot cope with the > arithmetic. Thus you are stuck, since none of the tools is powerful enough. This analysis is unfortunately correct, but fortunately the conclusion is too pessimistic. This is indeed an issue that I realized before on float arrays, and I implemented a solution in Jessie so that Gappa can prove the goals. Unfortunately the same treatment should have been done to structs, but wasn't. Still, there is a workaround, but using temporary scalar variables to help the provers. A solution is attached. It is heavy but I have no simpler solution to propose. In an ideal world there should exists a SMT solver able to handle the theory of floats natively. (This may happen in the future !) - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: siteZero.c Type: text/x-csrc Taille: 451 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/4da217fd/attachment.c>