The reason the numbers are not fixed is that the kernel knows whether or not an object type is valid by checking a range. For example one of the first checks in the decode untyped path is /* Is the requested object type valid? */ if (newType >= seL4_ObjectTypeCount) { userError("Untyped Retype: Invalid object type."); current_syscall_error.type = seL4_InvalidArgument; current_syscall_error.invalidArgumentNumber = 0; return EXCEPTION_SYSCALL_ERROR; }

From that point on it is assumed that the object type exists and is valid. The only further distinction that will be made is whether it is an arch specific object type or not.

It is a bit of a dumb restriction, but that is the way it is right now. Unfortunately I don't see any way of making things easier for you. Defining 'unused' types to high values was just done to allow a symbol to exist at user level and attempt to prevent the need for excessive #ifdef'ing of code. Adrian On Sat 07-Jan-2017 11:19 AM, Corey Richardson wrote: Actually, I think I'm mistaken? I see there are #define's for those config-dependent objects. I guess I should get out of the habit of reading kernel_final.c On 01/06/2017 07:01 PM, Corey Richardson wrote: Right now, object type numbers vary based on the kernel config (eg, CONFIG_VTX) etc. This is a huge source of pain for the Rust userspace libraries which don't integrate with seL4's build system. Is it possible for those enums to explicitly label every potential object type for a given architecture with a fixed number? _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel