Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] label L required?
- Subject: [Frama-c-discuss] label L required?
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Sun, 3 Nov 2013 19:53:22 +0100
- In-reply-to: <12EDDE98-B4F4-4694-91E5-C99536E31663@udel.edu>
- References: <12EDDE98-B4F4-4694-91E5-C99536E31663@udel.edu>
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
- Prev by Date: [Frama-c-discuss] Problems with ensures
- Next by Date: [Frama-c-discuss] Frama-c - wp on Windows/Cygwin
- Previous by thread: [Frama-c-discuss] Frama-c - wp on Windows/Cygwin
- Next by thread: [Frama-c-discuss] unable to interprete and trace jessie's output errors
- Index(es):