Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] call graph of kernel files
  • From: der.herr at hofr.at (Nicholas Mc Guire)
  • Date: Sat, 17 Apr 2010 19:54:58 +0200
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