--- layout: fc_discuss_archives title: Message 58 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 Faure wrote :
> 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 ?
I don't think so, but any way, you can just ignore these messages
since that size has no meaning from the C semantics.

Patrick.

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