Rafal Kolanski

After some discussion with Gerwin, I support the removal of this. If no one found ways to use it, and people forgot it exists, it's currently broken *and* we can't...

@michaelmcinerney : any reason this wasn't merged?

We already test 16 as it is the default. Did you mean another number?

Then you propose *adding* `1` and `2` to the weekly test? That makes sense. Other thoughts: - we need a branch with a commit that changes all the verified seL4...

Search+replace via regexp sounds like a good plan and will catch other arches should they appear. Yes, you're right, I'm conflating discussions. You proposed the floating commit for a platform...

@mbrcknl this might be of limited interest to you, and you might have other interesting ideas for the future, but I know you're very busy :) @michaelmcinerney : you wanted...

All PR issues should now be addressed. I rebased, and did a re-indent pass on Fastpath_Equiv. Because of the rebase I'll wait for tests to succeed (am running them in...

I'm fine with the names. Small comments, but nothing semantic.

Ah yes, I love this one, this C restriction screws our capability to give names to #define constants for verification, because they always end up as signed ints and so...

> On 64bit architectures, gcc still gives a 64bit enum when this macro is used which can be checked with a `sizeof` in a static assert. Ahh, aren't `int`s 64-bit...