--- layout: fc_discuss_archives title: Message 91 from Frama-C-discuss on September 2013 ---
Hi, We have run the example as suggested by Claude (http://proval.lri.fr/gallery/ScalarProduct.en.html). We used the example annotations in our code (attached) and the all VCs were proved. However, we have some doubts: 1. We have used the lemma bound_int_to_real but we did not understand how it works. Why the define NMAXR is used? 2. The variable j used in the loop was global in the legacy source code. However, the loop invariant was not proved (loop invariant \abs(p - sum(x,j)) <= j * BOUND). We changed the variable j to local and the loop invariant was proved. Does not the loop invariant work with global variable? Best regards, Nanci, Luciana e Rovedy 2013/9/7 Claude Marche <Claude.Marche at inria.fr> > > > > On 09/07/2013 10:56 AM, Claude Marche wrote: >>> >>> Alternatively, you can force the computation into float in sum >>> by modifying your axiom: >>> @ axiom sum2{L} : >>> @ \forall float *t, integer i, j; >>> @ sum(t,i,j+1) == (float)(sum(t,i,j) + t[j]); >>> But this is not a very good idea IMHO: as floating point addition is > > > A very bad idea indeed. > > - claude > > > _______________________________________________ > 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 -------------- A non-text attachment was scrubbed... Name: site003_43.c Type: text/x-csrc Size: 2255 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130912/a035966a/attachment.c>