--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on June 2010 ---
[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