Hi everyone,

I tried to make compile SEL4 + GENODE.
However, I must admit that this is a fail from my side.

The demo linux is compiling fine, but regarding sel4 I cannot make it work due to standard lib header missing.

To make it happen, I simply followed the tutorial from Norman (step 1).
I managed to make things work until make kernel command. After that I discovered that it was not executing the right kernel.mk file (there is one already delivered in latest sources), It compiles fine if I adapt a little bit CFLAGS.
Then the issue comes when trying to test the make run/test that is failing differently than what is described in the tutorial. (In fact, it is supposed to work in the tutorial)

It may be for sure a simple issue, but I don't really understand why I have this issue while compiling test and not the kernel...
The issue is the following:
error: no include path in which to search for stdint.h (and same for assert.h)

Do you think you could help me to figure out this issue, and maybe document it in your web page ?

Here is the trace below (I have a Ubuntu 14.04 LTS & x64 installation)
adg@...364....:~/dev/genode/genode/repos/base-sel4$ make run/test VERBOSE=
test -f "/home/adg/dev/genode/genode/repos/base-sel4/run/test.run" || (echo "Error: No run script for test"; exit -1)
~/dev/genode/genode/tool/run/run --genode-dir ~/dev/genode/genode \
                                     --name test \
                                     --specs "sel4 x86_32 x86 32bit" \
                                     --repositories "/home/adg/dev/genode/genode/repos/base-sel4 /home/adg/dev/genode/genode/repos/base" \
                                     --cross-dev-prefix "/usr/local/genode-gcc/bin/genode-x86-" \
                                     --qemu-args "" \
                                      \
                                     --include /home/adg/dev/genode/genode/repos/base-sel4/run/test.run
including /home/adg/dev/genode/genode/repos/base-sel4/run/test.run
building targets:  test/sel4 
spawn make test/sel4
make[1]: Entering directory `/home/adg/dev/genode/genode/repos/base-sel4'
checking library dependencies...
  Library platform
  Library syscall
  Library core_printf
    COMPILE  core_printf.o
/usr/local/genode-gcc/bin/genode-x86-g++  -ffunction-sections -fno-strict-aliasing -nostdinc -g -march=i686 -m32 -O2 -MMD -MP -MT 'core_printf.o core_printf.d' -Wall   -std=gnu++11 -I. -I/home/adg/dev/genode/genode/repos/base-sel4/src/base/console -I/home/adg/dev/genode/genode/repos/base-sel4/src/core/include -I/home/adg/dev/genode/genode/repos/base-sel4/src/base -I/home/adg/dev/genode/genode/repos/base/src/base/thread -I/home/adg/dev/genode/genode/repos/base-sel4/include -I/home/adg/dev/genode/genode/repos/base/include/spec/x86 -I/home/adg/dev/genode/genode/repos/base/include/spec/x86_32 -I/home/adg/dev/genode/genode/repos/base/include/spec/32bit -I/home/adg/dev/genode/genode/repos/base-sel4/include/sel4 -I/home/adg/dev/genode/genode/repos/base-sel4/include -I/home/adg/dev/genode/genode/repos/base/include -I/usr/local/genode-gcc/bin/../lib/gcc/x86_64-pc-elf/4.9.2/include -c /home/adg/dev/genode/genode/repos/base/src/base/console/core_printf.cc -o core_printf.o
In file included from /home/adg/dev/genode/genode/repos/base-sel4/include/sel4/arch/types.h:14:0,
                 from /home/adg/dev/genode/genode/repos/base-sel4/include/sel4/types.h:15,
                 from /home/adg/dev/genode/genode/repos/base-sel4/include/sel4/arch/functions.h:14,
                 from /home/adg/dev/genode/genode/repos/base-sel4/src/base/console/core_console.h:18,
                 from /home/adg/dev/genode/genode/repos/base/src/base/console/core_printf.cc:23:
/usr/local/genode-gcc/bin/../lib/gcc/x86_64-pc-elf/4.9.2/include/stdint.h:9:26: error: no include path in which to search for stdint.h
 # include_next <stdint.h>
                          ^
In file included from /home/adg/dev/genode/genode/repos/base-sel4/include/sel4/types.h:16:0,
                 from /home/adg/dev/genode/genode/repos/base-sel4/include/sel4/arch/functions.h:14,
                 from /home/adg/dev/genode/genode/repos/base-sel4/src/base/console/core_console.h:18,
                 from /home/adg/dev/genode/genode/repos/base/src/base/console/core_printf.cc:23:
/home/adg/dev/genode/genode/repos/base-sel4/include/sel4/types_gen.h:4:20: fatal error: assert.h: No such file or directory
 #include <assert.h>
                    ^
compilation terminated.
make[3]: *** [core_printf.o] Error 1
make[2]: *** [core_printf.lib] Error 2
make[1]: *** [gen_deps_and_build_targets] Error 2
make[1]: Leaving directory `/home/adg/dev/genode/genode/repos/base-sel4'
Error: Genode build failed
make: *** [run/test] Error 252

Thanks a lot in advance.