--- layout: fc_discuss_archives title: Message 10 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



HI !

 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. 

 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:

rtl26:/usr/src/linux-2.6.31# frama-c -cpp-command=\
"gcc -E -Wp,-MD,kernel/.sched.i.d  -nostdinc -isystem /usr/lib/gcc/i486-linux-gnu/4.3.2/include -Iinclude  -I/usr/src/linux-2.6.31/arch/x86/include -include include/linux/autoconf.h -D__KERNEL__ -Wall -Wundef -Wstrict-prototypes -Wno-trigraphs -fno-strict-aliasing -fno-common -Werror-implicit-function-declaration -Wno-format-security -fno-delete-null-pointer-checks -Os -m32 -msoft-float -mregparm=3 -freg-struct-return -mpreferred-stack-boundary=2 -march=i686 -Wa,-mtune=generic32 -ffreestanding -DCONFIG_AS_CFI=1 -DCONFIG_AS_CFI_SIGNAL_FRAME=1 -pipe -Wno-sign-compare -fno-asynchronous-unwind-tables -mno-sse -mno-mmx -mno-sse2 -mno-3dnow -fno-stack-protector -fomit-frame-pointer -Wdeclaration-after-statement -Wno-pointer-sign -fno-strict-overflow   -D'KBUILD_STR(s)=#s' -D'KBUILD_BASENAME=KBUILD_STR(sched)'  -D'KBUILD_MODNAME=KBUILD_STR(sched)' "\
 -cg-init-func=schedule -cg sched.dot kernel/sched.c

 this seems to actually work - giving me quit interesting output:

[cg] beginning analysis
[kernel] preprocessing with "gcc -E -Wp,-MD,kernel/.sched.i.d  -nostdinc -isystem /usr/lib/gcc/i486-linux-gnu/4.3.2/include -Iinclude  -I/usr/src/linux-2.6.31/arch/x86/include -include include/linux/autoconf.h -D__KERNEL__ -Wall -Wundef -Wstrict-prototypes -Wno-trigraphs -fno-strict-aliasing -fno-common -Werror-implicit-function-declaration -Wno-format-security -fno-delete-null-pointer-checks -Os
-m32 -msoft-float -mregparm=3 -freg-struct-return -mpreferred-stack-boundary=2 -march=i686 -Wa,-mtune=generic32 -ffreestanding -DCONFIG_AS_CFI=1 -DCONFIG_AS_CFI_SIGNAL_FRAME=1 -pipe -Wno-sign-compare -fno-asynchronous-unwind-tables -mno-sse -mno-mmx -mno-sse2 -mno-3dnow -fno-stack-protector -fomit-frame-pointer -Wdeclaration-after-statement -Wno-pointer-sign -fno-strict-overflow   -D'KBUILD_STR(s)=#s' -D'KBUILD_BASENAME=KBUILD_STR(sched)'  -D'KBUILD_MODNAME=KBUILD_STR(sched)'   kernel/sched.c"
include/linux/rwsem.h:186:[kernel] warning: Return statement with a value in function returning void
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
...
kernel/sched.c:10902:[kernel] warning: CALL in constant
kernel/sched.c:10902:[kernel] user error: doPureExp: not pure
kernel/sched.c:10902:[kernel] user error: Length of array is not a constant: 1 - 2 * tmp_0
[kernel] user error: Error during linking
[kernel] user error: your code cannot be parsed; aborting analysis.
[kernel] Frama-C aborted because of an invalid user input.

 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... so it might not a frama-c problem, but maybe someone has experience of dumping kernel sources - or am I simply passing the cpp command incorrectly ?

 Any hint how to do this ? 

thx!
hofrat