On Tue, Jun 16, 2015 at 5:42 PM, Adrian Danis <Adrian.Danis@nicta.com.au> wrote:
The seL4 kernel itself does not need anything for running C++ support.
However, ......
give you a bit of insight into what is required for a proper C++ port.
Recall that the important part is application binary application calling conventions. Once an ABI is understood a lot can be done. The micro kernel has calling conventions and services. Applications need to live on top of this. For students the easy trick is to write in the high level language but save the assembly output file and inspect how the function is passed data and how it returns results. When mixing compilers this is a challenge. With gcc there is a common set of ABI services. Mixed vendor compilers are more complex. One issue is the set of choices that the language specification gives to compiler authors. In FORTRAN there are a couple famous vendors and they encode and test for True & False differently. The result is shared library trouble. Much can be sorted with cautious test cases. -- T o m M i t c h e l l