Hello,
I am currently attempting to use the seL4 Benchmark tool. After going through
the menuconfig (kernel -> build options -> Enable Benchmarks -> Track threads
and kernel utilization time), I attempt to rebuild, and get a host of errors:
In file included from
/home/chrisguikema/gdbtest/kernel/include/compound_types.h:16:0,
from /home/chrisguikema/gdbtest/kernel/include/types.h:15,
from /home/chrisguikema/gdbtest/kernel/src/api/faults.c:14:
/home/chrisguikema/gdbtest/kernel/include/object/structures.h:249:5: error:
unknown type name 'benchmark_util_t'
benchmark_util_t benchmark;
And a lot more, but all along the "not a structure or union" line, which makes
me think that either the header file isn't being linked properly, or the
#ifdefs aren't working for everything.
Did I do something improperly in my setup?
Thanks,
Chris Guikema
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
