Hi Chris,

Thanks for reporting this. Looks like some new changes to the kernel introduced circular dependencies that prevented the header that defines benchmark_util_t from getting included. Should be fixed now (530852b).

Cheers,

Hesham

________________________________ From: Devel devel-bounces@sel4.systems on behalf of Chris Guikema Chris.Guikema@dornerworks.com Sent: Wednesday, January 11, 2017 8:42 AM To: devel@sel4.systems Subject: [seL4] Using the seL4 Benchmark Tool

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