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,
Matthew Scaperoth
Jr. Programmer Analyst
The George Washington University
Academic Technologies
Tel: 202-994-6907
