Gerwin Klein

The `FPU0002 ` test seems to be passing, but as expected `IPC0028` is failing.

We should only merge this one after a fix for `IPC0028` is merged (e.g. something like https://github.com/seL4/seL4/pull/986).

The offending commit that introduced these was https://github.com/seL4/sel4test/commit/d07b2383b563015d8e7dad5c587493be01cf8b3c from 2017. I've now added a commit on top that disables IPC0028 so we can at least re-enable the other test. I'll...

The gitlint check is complaining about a too-long title (max 50 characters). Please shorten, but instead provide context and background/reasoning for the change in the body of the commit message...

@Indanz can you please check if you're now happy with Ivan's changes?

While we're expecting the tests to currently fail, it looks to me like some of the operations are returning a different kind of error, e.g. cap lookup fault instead of...

(rebased and tweaked under which configs we should expect an error)

Now passes on all runs for all boards. We still need to fix up the review comments, though.

This might have verification impact for the system initialiser. @corlewis do we need to do anything special in the tools or is this just excluded in spec wellformedness for sys-init?...

@corlewis I'd be fine with merging https://github.com/seL4/l4v/pull/716 and this PR here. It's relatively rare that we update these slots, so it shouldn't be too much of maintenance burden.