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