Gerwin Klein
Gerwin Klein
This re-enables test IPC0028 which was found effectively disabled since 2017 and broken in #89. We can use this PR for checking potential fixes. See also https://github.com/seL4/seL4/issues/941 and https://github.com/seL4/seL4/pull/986
Do not perform cache flushing in clearMemory. Instead flush the cache only for those object types where it is necessary, and only when the object is retyped, not when the...
We no longer guarantee the invariant that the replyObject reference is `NULL` when the thread state is not `BlockedOnReceive` or `BlockedOnReply`. It is likely that this invariant was true in...
Require cython < 3, because >=3 breaks the install for pyyaml at build/install time for more recent python versions. The cython < 3 fix only works on pyyaml < 5.4,...
Currently the preprocess test is looking at the AST diff between the verification manifest version of seL4 and the PR version of the code. When the verification manifest is in...
While the rangeError types in `SchedControl_ConfigureFlags` correctly return the expected ranges, it would be nice if the `userError` message strings also reported those ranges to make them more discoverable. E.g....
With recent proof improvements the proofs now apply to further platforms in the ARM, ARM_HYP and AARCH64 configurations. The rest of the config values are kept on whatever the default...
Since PR #1206, the test MULTICORE0002 is failing on the board OdroidC4 (and only on this board) in the configuration debug_MCS_SMP_clang. It's unclear why, we have so far not been...
The GIC platforms use `irq_t` for `irqInvalid` -- bring remaining AArch32 platforms in line with that. `irq_t` is an unsigned type (when it is an integer) and enum constants are...
Verification update for PR seL4/seL4#1289 where we defer the cache flush from untyped reset to the actual retype operation, which means that only flushes that are actually necessary will be...