Gerwin Klein

Just as another note: storing rights in objects is usually a red flag, because rights are usually associated with caps and storing them anywhere else but caps opens up time-of-check/time-of-use...

> This can occur currently in non-mcs right? I think the TOCTOU issues are inherent with endpoints. We already expect cancelBadgeSends to be called explicitly if a badged endpoint is...

After conversation with @kevinelp and @gernotheiser just now on access control in MCS in general, I think we should bump this up and merge. (We arrived at the same conclusion...

> @lsf37 I tuned out at a crucial moment in this morning's developer hangout, when you were talking about making an RFC for this and #940. > > Was the...

Assigning this to @corlewis who is involved in that proof.

For context, this is what such an enum declaration looks like after preprocessing: ```c typedef enum { SEL4_BOOTINFO_HEADER_PADDING = 0, SEL4_BOOTINFO_HEADER_X86_VBE = 1, SEL4_BOOTINFO_HEADER_X86_MBMMAP = 2, SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP = 3, SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER...

An `int` on 64 bit is still 32 bits, a `long` is 64.

The standard says "implementation defined" for what the `enum` type actually ends up with, it just says that the constant expressions have to fit into an `int`. The C parser...

> Did you read the comment above SEL4_FORCE_LONG_ENUM? Its goal feels sound, i.e. to stop clever compilers from picking something smaller than int. However yes, the name is misleading, as...

> For today, what are you going to do with this? We could potentially add an annotation to inform the C parser to override the size of a specific enum...