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

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