--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] call graph of kernel files



Hello,

> ?Using frama-c to generate call graphs - works like a charm for user-space
> ?but I have serious problems getting it to work on kernel code.

The linux kernel is notorious for containing gccisms, but the CIL
front-end that Frama-C is based on is supposed to accept most gcc
syntax extensions (they are not necessarily understood, viz asm
statements, but at least the front-end should not choke on them).

> ?Configure the kernel as needed and ran an initial make kernel/sched.i to
> ?get all the dependencies in place. Then manually removed kernel/sched.i and
> ?ran the command again to dumped the preprocessor command with
>
> ? ?make V=1 kernel/sched.i
>
> ?finally I simply passed that to frama-c as follows:

Well done.

> include/linux/rwsem.h:186:[kernel] warning: Return statement with a value in function returning void

I don't have a line 186 in my include/linux/rwsem.h, but I think we
can trust CIL on that one: it has probably caught some oddity in a
corner in the linux codebase.

> include/linux/gfp.h:223:[kernel] user error: Length of array is not a constant:
> 1 - 2 * ! (! ((59624 >> bit) & 1))
> include/asm-generic/tlb.h:64:[kernel] warning: CALL in constant
> include/asm-generic/tlb.h:64:[kernel] user error: doPureExp: not pure

gfp.h line 223 contains call to a macro named BUILD_BUG_ON.

In file include/linux/kernel.h, near line 678, you may find something like:

/* Force a compilation error if condition is true */
#define BUILD_BUG_ON(condition) ((void)sizeof(char[1 - 2*!!(condition)]))

I will leave the question of whether this is valid C99 to the
philosophers. I suggest replacing this definition and similar ones
around the same point with

#define BUILD_BUG_ON(condition) ((void)0)

> [kernel] user error: Error during linking
> ?but as can be seen it bailes out with the error during linking and consequently does not generate a call graph. What I don't understand is why gcc -E is trying to link at all

The allusion to "linking" refers to the linking phase of CIL. Whereas
C compilers implement separate compilation (and, by the way, fail to
detect some typing errors because object files are not typed), Frama-C
analyses whole projects in which the symbols in separate files that
are supposed to be the same have been conflated.

Good luck

Pascal