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] [Fwd: Meaning of warning]

Christele,

> I cannot figure out what this message means: ALE.c:342:[kernel] 
> warning: Cannot represent the length of array as an attribute.
> I got this message 135 times on my application.
> Does any one know about this message ?
>

As you know, the function prototype
void foo(int x[10]);
is equivalent to
void foo(int *x);

Frama-C tries to convert the array size into an attribute in order to 
don't loose the information.
The previous prototype is pretty-printted as follow by Frama-C:
void foo(int * /*[10]*/ x);

In your case, it seems that Frama-C cannot convert the array size.
For exemple, this can occur with integers needing more than 64bits for 
their encoding.
What kind of size expression do you have?

Patrick.

-- 
Patrick Baudin,
CEA, LIST, DILS, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072