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

On 07/07/15 18:13, Wink Saville wrote: