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: http://os.inf.tu-dresden.de/fiasco/build.html) provide all the necessary debug information in it?
the generated hello.iso file is an ISO CD-ROM image (see http://en.wikipedia.org/wiki/ISO_image), 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.
Cheers, Bjoern