Gerwin Klein

The PR #1010 now adds a comment in the generated `_gen.h` file that points back to the original `.bf` files before preprocessing.

The plan is to discuss Nick's proposal, and if we're happy with going with that, to work on this PR to make the JSON export robust. In particular, we probably...

Closing this PR as superseded by #975. Thanks @ahmedcharles for starting this discussion!

Rebased and squashed in preparation for the proof update.

You're right. I'm closing this issue specifically for `stat`. I'd say `json` export is a separate issue we should think about, and we could re-open or create one for that...

The `irq` parameter question is tracked separately in #991 now, but I think it would still make sense to move the [getActiveIRQ line](https://github.com/seL4/seL4/blob/a7fcda426754091f66351942e18d964943016153/src/api/syscall.c#L41) to just before `irq` [is needed](https://github.com/seL4/seL4/blob/a7fcda426754091f66351942e18d964943016153/src/api/syscall.c#L49) before...

Ok, great. Let's do both of these. I'll put up PRs for C. Can I leave the Isabelle side to you?

Coming back to this after staring at the region code more and documenting it in #1007: the memory region types are definitely with exclusive end, we should not change that...

@axel-h you mentioned in the comment above that you've seen the region end used as inclusive in the code. Do you remember where? It'd be good to fix these and...

Doesn't seem to be bad at all, the only one I randomly saw in the logs was for AM335X (beagle bone black): ``` Bootstrapping kernel available phys memory regions: 1...