--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on June 2015 ---
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>