--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2013 ---
Hello, Le jeu. 31 oct. 2013 13:42:48 CET, Stephen Siegel <siegel at udel.edu> a ?crit : > There is no label L in the source (since I removed them), but in the > intermediate file mean2b.jc, an "{L}" was added to axiom sum1: > axiom sum1{L} : > (\forall doubleP[..] a_1; > (\forall integer n_0; > ((n_0 >= 1) ==> > (sum(a_1, n_0) == (sum(a_1, (n_0 - 1)) + (a_1 + (n_0 - > 1)).doubleM))))) --- > > > /*@ axiomatic sums { > @ logic real sum{L}(double *a, integer n); > @ axiom sum0{L}: \forall double *a; sum{L}(a,0)==0.0; > @ axiom sum1{L}: \forall double *a, integer n; n>=1 ==> > @ sum{L}(a,n)==sum{L}(a,n-1)+a[n-1]; > @ } > @*/ In fact, if you do a frama-c -print on your source file, you'll notice that this label is added by the type-checker. Namely, this feature has been added to avoid writing too many {L} in logic definitions. You're only required to explicitely name logic label parameters if you want to use more than one, i.e. define a function or predicate that relate two or more states. Otherwise, they will be added as needed, that is whenever a memory access occur, which is the case for sum1 (a[n-1], since a is a pointer and not a (logic) array), but not for sum0 (as long as sum itself is not declared with an {L}). In fact, you should declare sum with a logic parameter, as it indeed relies on the memory (and since it is a declared function, you cannot rely on the mechanism above to add it for you, since there's no definition to infer the need for a logic label from). Best regards, -- E tutto per oggi, a la prossima volta. Virgile