--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] label L required?



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