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