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