--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on April 2010 ---
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