Hello All,

First I wanted to say thank you for this dev forum. The more I learn about SeL4 the more I am amazed with how well it is written.

I am working on a 32-bit Ubuntu 14.04 and I would like to run your individual test suites in the sel4-manifest with a 32-bit build. Specifically some of the tests from the https://github.com/seL4/sel4test/tree/master/apps/sel4test-tests/src directory. For example, I'd like to alter the code a little bit and run qemu to output cycle time for IPC or memory mapping. So potentially I would boot up the image, the files would load and I would get an output saying "Intra-as IPC 151 cycles" or something along those lines after the test was automatically run.

I was reading through the files and noticed that the main.c accepts arguments to say which test I'd like to run using the find_test() method with the argv passed in. I am now trying to find a way to use the main.c file in sel4test-tests to achieve the build I am after.

I also noticed that a .bin file and a another file in stage/ia32/pc99/bin/sel4test-tests are generated when you run the first top-level make after the configuration. So I have tried booting the sel4test-tests file in qemu with

qemu-system-i386 -m 512 -serial stdio -kernel images/kernel-ia32-pc99 -initrd stage/ia32/pc99/bin/sel4test-tests

but nothing happens. My thought process was that it could replace the driver image for ia32 pc99 (sel4test-driver-image-ia32-pc99) .

So I am missing a piece here (or pieces?). I am not sure if there is a Makefile that I can alter to include only a specific test, or if it's something else entirely. I'd be happy to clarify what I aim to achieve or details about my system if necessary.

Also, I am really enjoying the code that generates these tests in the main.c file mentioned earlier. I feel like it is a much more graceful solution to running these tests than other l4 systems I've worked with.

Thanks again,

Matt