--- layout: fc_discuss_archives title: Message 57 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]



BAUDIN Patrick wrote:

>
> 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?

It is probably a dynamic size and the application is too large to know 
exactly.
Is there any way to avoid these messages ?
Ch

>
> Patrick.
>


-- 
Christele Faure-Simeoni
04 93 77 71 08
http://pagesperso-orange.fr/Christele.Faure/
http://www.safe-river.com/