Ben Leslie
Ben Leslie
Currently cmake_minimum_required` is called from most `.cmake` files. The exceptions are * `FindseL4.cmake` * `configs/*.cmake` The versions are either 3.8.2 or 3.7.2 (mostly 3.8.2). It seem unnecessary to call this...
I'm in deeper to the kernel than normal, so I could be wrong with this analysis. It appears that there is a difference between an 'invalid capability' which raise a...
In the method name of the document in some cases phrases are used (with spaces and capital letters) and in other places camel-case is used. For example, we have "Asid...
This bit of code from `syscall.c:handleInvocation` ``` if (unlikely(length > n_msgRegisters && !buffer)) { length = n_msgRegisters; } ``` has me stumped. I think, it is checking if there is...
As far as I can tell the following: ``` /* Minimum size of a scheduling context (2^{n} bytes) */ #define seL4_MinSchedContextBits 8 #ifndef __ASSEMBLER__ /* the size of a scheduling...
In some implementation (rockpro64) the `CR` is sent after the `LF`, while in others (such as imx) it is sent prior to the `LF`. I *think* it should be sent...
The parameters for the `set_timeout` function are documented in `platsupport/ltimer.h` however the semantics are not very clear. Specifically, what is the correct behaviour if called with a time that is...
The exact semantics of this don't appear to be documented anywhere that I could find. The semantics I assume is that if we ever have a timer overflow then some...
The NULL pointer check in `gpt_init` should be moved prior to the use of the pointer.
In the `allocate_register_callback` function there is an assert: ``` assert(curr_num == 0); ``` This does not seem appropriate. I'd suggest that this should return an error (in the same way...