Gerwin Klein

There are currently 85 such warnings on the master branch, many of which are versions of `unsigned conversion from 'int' to 'syscall_t'` at different points in `syscall.c` (all safe). Some...

> A significant amount of tests are disabled as I couldn't get the ARM generic ltimer implementation to play nice, any test that required the timer to sleep would not...

> Is the preprocess failure suggesting changes to me? Not sure I understand what it's trying to say. It's showing the code changes that are visible to verification and that...

> > Is the preprocess failure suggesting changes to me? Not sure I understand what it's trying to say. > > It's showing the code changes that are visible to...

I don't think we should do this, at least not for this many of the workflows. These are cheap and quick runs and it makes the workflows unnecessarily complicated when...

> @lsf37 is this still awaiting verification? Yes -- I wasn't sure if the discussion was settled or not. If this is the version we want, I can have a...

It turns out, we need to add padding to the VCPU struct now so that it remains packed. I'll push a commit for that once the proofs have passed.

(Rebased in preparation for merge when the proofs on https://github.com/seL4/l4v/pull/723 have passed)

The proofs are fine, but this PR broke the CAmkES VM, see the runs in

Still seems to be breaking after merging seL4/seL4_projects_libs#125 with the same error: ``` [email protected]:704 module name: plat Loading Kernel: 'linux' Loading Generated DTB seL4 called fail at /github/workspace/kernel/include/arch/arm/armv/armv7ve/armv/vcpu.h:628 in function...