how to debug fiasco kernel

Björn Döbel doebel at
Wed Apr 3 12:26:20 CEST 2013

Hi Keqin,

>           Thank you very much for your timely reply, but I still want to know if 
> I must recompile the source code to create another kind of image which can be 
> used for debugging(like vmlinux)? Does this image hello.iso(generated from 
> official guide: provide all the 
> necessary debug information in it?

the generated hello.iso file is an ISO CD-ROM image (see, which contains all necessary
binaries to boot a certain Fiasco.OC setup (e.g., the bootstrapper, the
kernel, and the hello world application).

For debugging using BochsGDB or QEMU's GDB server you will need a single
binary. For the Fiasco.OC kernel, you will find two binaries in the
kernel's build directory. The 'fiasco' binary is the one that gets
loaded, but it does not contain debug info. The 'fiasco.image' binary is
the same binary but with debug information attached. So if you want to
debug the kernel, tell GDB to load the latter binary.

For L4Re user-level applications (such as hello) you will find the
respective binaries in the L4Re build directory (bin/<arch>/<L4API>).
These binaries are not stripped by default so you can directly use them
with GDB.


More information about the l4-hackers mailing list