Hi Wink,
I started reading the commit to the kernel (
https://github.com/winksaville/seL4/commit/c25d8e1af9126e242e220164e30a5ef6c1b132b9)
and I liked a lot of it, but I still have a few
comments.
* You appear to have added several files to the top
level of the include directory and prefixed them with
'sel4_' to try and prevent header name collisions. Why
not put them in the 'sel4' subdirectory like we already
do (here and in all our other libraries)? In doing this
you have left headers, for backwards compatibility I
assume, in the sel4 directory that then include new ones
in the top level directory. This all makes no sense to
me.
* I still do not like the way you are implementing
assert. In my last e-mail I said to define
libsel4_assert to __assert_fail and then let the
application be responsible for providing __assert_fail.
The main motivation for doing this is that in the case
that you *are* using a C library you need to do nothing
to handle this change, as it will have a link time
implementation of __assert_fail.
* Why is there a prototype for halt in libsel4? It seems
to exist because it is referenced by your libsel4_start
routines. Neither of these should be in libsel4
* I do not mind a definition of NULL in libsel4, but you
seem to have renamed all the uses of NULL->seL4_NULL
and then left the definition of NULL in
sel4_simple_types.h anyway. Either use define NULL or
seL4_NULL, not both
* sel4_vargs.h seems to be left over from some previous
attempt at this change, but I don't see it referenced
anywhere in libsel4 itself
The rest of the changes all good, including the
syscall_stub_gen and bitfield_gen changes.
What I would keep in mind with this change is that I
would hope that applications that do use a C library to
require zero modifications with this change.
Adrian