[seL4] Issues about compile C program