Debugging seL4 elfloader using lauterbach failed to step into c code

seL4 kernel
1

Hi Team,

Setup:
seL4 Version : 13
Debugging: Debugging ELFloader code
Platform: arm64
Build Type: CMAKE_BUILD_TYPE:STRING=Debug

I have compiled the seL4 for arm64 based hardware and able to run seL4 kernel from elfloader successfully.
For Debugging i have enabled debug symbols as mentioned above. Now on target, i have attached lauterbach to debug further. I am able to see all symbols and breakpoint is getting hit from break.list, when i tried to set breakpoint from c code. But unfortunately step into c code is not working. if i set break point from multiple c files, still breakpoint is gettting hit, but step into c code is not working, only working in assembly.

Is seL4 debugging tried with JTAG ?

2

You may be the first person doing this.

Maybe enabling CONFIG_HARDWARE_DEBUG_API in seL4 makes it work? Or, if already enabled, disabling it?

I wouldn’t expect a hardware debugger to need any help from the running code though.

3

What is the format of the elfloader file being loaded? On Aarch64 the elfloader is expected to be relocatable and could be placed in a different memory location by u-boot than what is defined by the elfloader’s ELF file.

4

Hi Indan,
Thanks for the info.
The config mentioned is for seL4 kernel. Issue is currently observed in elfloader code.