--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on June 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Error of having 0-length array



Thanks, Pascal. It is indeed not a good idea to learn Frama-C through a
complex project like pureftp. Will try some smaller examples first.

Best,
- Guanhua

http://www.cs.binghamton.edu/~ghyan

On Tue, Jun 9, 2015 at 5:53 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

>
> On Mon, Jun 8, 2015 at 10:07 PM, Guanhua Yan <ghyan at binghamton.edu> wrote:
>
>> Hi:
>>
>> I got this error when trying to use frama-c to analyze the pureftp source
>> code.
>>
>> /usr/include/x86_64-linux-gnu/bits/fcntl-linux.h:316:[kernel] user error:
>> Length of array is zero. This extension is unsupported
>>
>> Any clue about this error?
>>
>
> As the message says, arrays of length zero do not exist in C (C99
> 6.7.5.2:1 “If the expression is a constant expression, it shall have a
> value greater than zero”). Frama-C, although it supports many nonstandard
> constructs, does not support this particular nonstandard construct.
>
> On a more general note, you are wasting your time trying to analyze
> software as complex as pureftp without having first gotten used to Frama-C
> on smaller examples. As an example of a strategic mistake that you should
> have learnt to avoid with smaller examples, you are pre-processing with a
> system header from your system:
> /usr/include/x86_64-linux-gnu/bits/fcntl-linux.h. This never ends well. If
> the software uses system headers that you cannot replace with ones you
> write yourself and provide specifications or stub for, you are not ready to
> analyze it with any of Frama-C's plug-ins.
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150610/c522d289/attachment.html>