Re: [seL4] Try two for libsel4 not having a dependency on libc

3 Jul 2015


      One other note, this isn't done. It still needs to be integrated with muslc
(libc) and at a minimum seL4_Halt needs to be properly implemented. And I'm
sure there will be plenty of other changes needed but I hope we're closer.

On Thu, Jul 2, 2015 at 5:11 PM Wink Saville  wrote:
...
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc3 is try
#3, I've pasted the commit message below as it tells the story, let me know
what you think:
libsel4 with no libc dependency.
The primary changes are introducing sel4_types.h and removing std*
types
    plus porting assert and printf code from the kernel to libsel4. All of
    this means the code within libsel4 does not overload any typical libc
    entities. So now libsel4 uses types like seL4_Uint32 ... instead of
    uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt it was more
    consistent with the names of the entities within the files.
The only new library is libsel4_benchmark and since it consists of just
    sel4_benchmark.h we might want to move that back into libsel4. I would
    have liked to move out libsel4_assert, libsel4_printf and
libsel4_putchar
    but since asserts are used by low level generated code I couldn't come
up
    with a good way of doing that.
Finally, the only file modified that effects kernel code is
    kernel/tools/bitfield_gen.py. It needed to be modified as it generates
    files for both kernel and user space. And for user space the generated
code
    (types_gen.h) needed to use the new types and asserts. The changes
should
    not change what is generated for the kernel and I did a comparison of
    kernel_final.{c|s} before and after my change and the only differences
    were time stamps
-- Wink
On Mon, Jun 29, 2015 at 7:07 PM Wink Saville  wrote:
...
Will do.
On Mon, Jun 29, 2015, 7:05 PM Anna Lyons  wrote:
...
Hi,
...
Currently there is at least one known problem, I modified
bitfield_gen.py so types_gen.h has no asserts since at the moment the
kernel uses assert and userspace is libsel4_assert. We could either do
something like I've done and remove them or change the kernel to use
libsel4_assert or something else.
The asserts are really important to avoid horrible bugs when using
functions created by the bitfield generator, so if we go ahead with this
let's make sure they survive in some form.
Cheers,
Anna.
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel