Gerwin Klein

> If the only reason why gcc-7 doesn't build anymore is because we started using the __naked__ attribute on x86, then I'd suggest we instead stop using the attribute and...

> Which gcc version does binary verification assume? :) That is an excellent question. @zaklogician or @mbrcknl what gcc version were you guys using?

Fwiw, I don't see any problem from the verification side with the proposed change, I don't think we have any properties/invariants that would break because of it. It'd just be...

The PR introduces 2 new sorries further down in AInvs, so the theory linter warnings are expected.

Cool, review feedback address and rebased. Will merge when tests pass.

@michaelmcinerney it might make sense to do a test merge with MCS for this one to see if it leads to massive conflicts or not. Unless the perl/sed path is...

For some reason the GitHub tests didn't trigger apart from the DCO. I'm very confused by this -- shouldn't be possible and the tests seem to be working fine on...

> > Good to bring them in sync again. A lot of these look like wrong indentation got fixed on the MCS side. No problem reverting this here, but we...

> please don’t contact me personally, use ***@***.*** as I won’t have the time to look your issues myself. Gernot I suspect Gernot means the [developer mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/) (GitHub masks...

And it seems to be catching a bunch of divergences. If they are small enough those would be good to fix in the same PR.