--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on September 2013 ---
Hi, We have tried to complete the specification of the same source code (attached). After inserting the two annotations below, there were some not proved VCs (401/405): assigns Gbl_Eventos[9].Gbl_Ativo; ensures (pri == 1) && (ID == 1) && (\old(Eventos[9].Ativo) == 0) && average > 12.0 ==> Eventos[9].Ativo == 1; In order to write this postcondition we followed the sequence of the statements in the source code. What is wrong with these annotations? Best regards, Nanci, Luciana, Rovedy 2013/9/14 Claude Marche <Claude.Marche at inria.fr> > > > On 09/12/2013 08:06 PM, Rovedy Aparecida Busquim e Silva wrote: > > 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? > > the lemma says the if some integer n is less or equal 3, then when > converting it to a rel number the result is less or equal 3.0. Seems > stupid but needed to help provers... > > > 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? > > It should not make any major difference. However since the context of > the VC would be a bit different (e.g. not the same order of hypotheses), > you may need to increase a little the time limit given to the prover. > > I tried your example and I've been abble to prove it, both in case j is > global and when it is local. Although, I needed to modify a bit the > annotations: removing the "loop assigns p,j" that disturbs Jessie, and > replacing "sum(x,...)" by "sum(x+0,...)" because it is refused by > Frama-C kernel. I'm using Frama-C Fluorine 20130601 + Why 2.33 + Why3 + > provers Alt-Ergo, CVC3 and Gappa. > > Hope this helps, > > - Claude > > > > 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 > >> > >> > >> _______________________________________________ > >> 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/20130916/444c2731/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: site003_53.c Type: text/x-csrc Size: 2879 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130916/444c2731/attachment.c>