Gerwin Klein
Gerwin Klein
Currently a lot of VCPU lemmas are mixed into ArchVSpace. It would probably make sense to collect these in a separate file (and also see which other VCPU lemmas are...
While discussing the monadic rewrite framework in #487, we realised that `monadic_rewrite` demands that failure on the concrete side implies failure of the abstract side. This is a general refinement...
The `camkes-cli` tool is unused and basically bit-rotted. It should either be resurrected and brought up to date (might not be hard), or be retired/put on hold officially. The tool...
`style-cmake.sh` resets the file mode, using `cmake-format` with `-i` which always produces `644` files. It'd be nice to keep the original file mode, since we have some cmake files that...
Every once in a while we're getting a failure in the CI simulation run. Since it's simulation, we can exclude hardware glitches and since it is working most of the...
I thought I had seen this building successfully before, but it seems that was not the case. Error message is: ``` In file included from /github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm/armv/armv8-a/sel4bench/armv/private.h:9, from /github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm/armv/armv8-a/sel4bench/armv/sel4bench.h:10, from /github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm/sel4bench/arch/sel4bench.h:12,...
In config `ODROID_XU4_debug_hyp_MCS_clang_32` (and apparently only this config and only on clang), ODROID_XU4 is failing the test `CACHEFLUSH0001`. The configuration is disabled for tests for now. It looks like this...
The test is already marked as `flaky`. If at all possible we should make this non-flaky. There is also a comment inside the test that says it can never properly...
Logging this here, because I have not seen this fail before and it is likely (very) intermittent only -- `TIMEOUTFAULT0002` got stuck on [this](https://github.com/seL4/seL4/actions/runs/7718784961/job/21046477513) run. The [corresponding commit](https://github.com/seL4/seL4/commit/91ec17c5bf29a4ef8b98b8f9769580b2442eb810) had no...
config_set is true for 1 and false for all other values, so it does not make sense to use with CONFIG_MAX_NUM_NODES. The two instances where this happened look like they...