--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on October 2013 ---
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 -------------- next part -------------- A non-text attachment was scrubbed... Name: siteZero.c Type: text/x-csrc Size: 352 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131004/2d5d7705/attachment.c>