Analyzing large projects with Frama-C

3
votes

I want to analyze a file from a large project to create a Program Dependence Graph using Frama-C, but keep getting odd errors such as:

/usr/include/bits/fcntl-linux.h:305:[kernel] user error: Length of array is zero. This extension is unsupported

If I try to use the libc implementation provided by frama-c, compilation fails due to missing headers such as sys/file.h.

I am trying to analyze files from the Lynx project, specifically the file in src/WWW/Library/Implementation/HTTP.c, using GCC version 4.8.1

What I really need is to be able to generate a PDG for this source file (which of course has various dependencies) but I think if I could get even a somewhat incomplete graph by skipping over undefined functions, that would be a great first step.

1
frama-c
Perhaps you need to tell frama-c the location of the headers. This is done by setting the environment variable like this: export CPP='gcc -C -E -I/path/to/headers -I.' - Cristiano Sousa
@CristianoSousa True (in addition, GCC option -nostdinc tells GCC not to use the system's headers at all), but it seems the OP already knows this. It is true that some widely used headers are not provided in Frama-C: the Frama-C provided headers are the bare minimum C-mandated ones (and perhaps some POSIX ones). - Pascal Cuoq

1 Answers

4
votes

You need to provide your own "file.h" file in a directory "sys" placed anywhere in the path GCC searches when pre-processing for Frama-C.

For reference, here is the implementation of sys/file.h on another system. You may also be interested in this other StackOverflow question about sys/file.h.

For Frama-C's value analysis, assigns clauses alongside the prototypes go a long way:

/*@ assigns *f \from ui, s, *fo; */
void finit(struct file *f, u_int ui, short s, void *p, struct fileops *fo);

Note that I have no idea what function finit() does and whether the above is a correct assigns clause for it. In fact, this is the whole point: neither does Frama-C out of the box, and since this lowish-level, lessish-portable system call is used in the code you wish to analyze, someone will have to know. I am afraid it is going to have to be you. On the plus side, you only need to provide the types, macros and function prototypes that the code you wish to analyze uses.