The html5validator is complaining about duplicate IDs in html produced
from the markdown:
- `channel` occurs twice, once explicitly defined and once as a
later heading. Rename explicit reference to #channels to match up with
heading name.
- `libmicrokit` occurs twice as a heading, one with explicitly defined ID.
Rename the second one to #libmicrokit_internals to disambiguate.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit adds support for building the seL4 kernel, loader, monitor,
and libmicrokit with LLVM (Clang, LLVM and ld.lld). Passing --llvm
should instruct the tool to build everything with with LLVM.
Clang/RISC-V don't implement or need -mstrict-align
Also fix a trivial error adding single quotes within a string.
Signed-off-by: Hesham Almatary <heshamalmatary@capabilitieslimited.co.uk>
This would otherwise give the warning
platform maaxboard supports multiple architectures, none was given
defaulting to: aarch64
on platforms which support multiple architectures, for instance, the
maaxboard which can be built for aarch64 and aarch32. This seems to have
been fine because the first option is always the 64-bit option, but this
is probably unlikely to be guaranteed.
For the CMake Builds for sel4test et al, this is set in
cmake-tool/helpers/application_settings.cmake.
Signed-off-by: julia <git.ts@trainwit.ch>
Previously I did not turn this option on by default because
I thought it would make the kernel proofs not apply anymore.
In reality this is only true really when a user makes use
of the SMC feature. Most users probably will never have to enable
it and the ones that that do will no longer have to patch Microkit
to enable it.
I've added a warning about using SMC calls in the manual to make users
aware of the implications of using this feature.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
QEMU virt AArch64 won't have U-Boot to initialise the UART for
us. QEMU doesn't care and will happily output to the UART even
if it's disabled, however if you add `-d guest_errors` to your
QEMU invocation, you will get a bunch of QEMU complaints saying
you are outputting to the UART while it is disabled. This
will fix that.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
A PD will have two sets of mappings in addition to what the
user has specified:
1. Mappings for the ELF
2. Mapping(s) for the stack region
Previously, it was possible to accidentally create an overlapping
between a user-specified mapping a mapping generated by the tool
automatically.
On ARM, this is quite subtle as seL4 allows overwriting existing
mappings resulting in no obvious error when this happens.
On RISC-V, this leads to an error upon booting due to seL4 *not*
allowing overwriting existing mappings with unmapping first.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
When creating CNodes, the `size` is the (log2) number of CSlots. When
creating SchedContexts the `size` is the (log2) size of the object in
bytes.
Signed-off-by: Mathieu Mirmont <mat@neutrality.ch>
With the changes to seL4 regarding reserving the SBI region
properly [1] it means we can no longer use 0x80200000
as a loader link address for this platform.
[1]: cf3a64b44c
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Ivan-Velickovic