Hey All,

First, thank you for your responses so far. This message board has been helpful with learning seL4. 

While we have been working to benchmark the seL4 system on bare metal we have run into some trouble trying to figure out how to get output to the console instead of serial. For our tests we are using the existing seL4test-manifest files and defining custom tests within the apps/sel4test-tests/src/tests/ipc.c file. We noticed that the test output will only go to serial. We have tested with and without the debug configuration. 

We would like to see all output go to console. We have tried to remove debug defines on the system call path for __arch_putchar() which seems to only affect the serial output. These system calls don't seem to affect the direction of the output, but only what is being output to serial. 

Is there a driver missing from the test libraries that defines the console output? Is there a specific way to output to console when working with tests.

To test these settings we are working with a 32-bit build and are using syslinux to create a bootable USB to test on bare metal. 

Regards,