English is currently available.
Ada & SPARK DISCUSSION
A device register uses the codes 1, 2 and 4 for three operating modes, so I declared type Mode is (Idle, Run, Fault); with for Mode use (Idle => 1, Run => 2, Fault => 4);. When I send Mode'Pos (Fault) to the device I get 2, not 4.
How do I obtain the actual code for a value, and how do I safely convert a byte received from the device back into a Mode when the byte might be something invalid such as 3?
'Pos returns the position number in the declaration, always 0, 1, 2 and so on, and is unaffected by a representation clause. The clause only changes the bit pattern stored in memory. That is why Mode'Pos (Fault) is 2 and Mode'Val (2) is Fault, whatever codes you assign.
With GNAT the simplest way to read the stored code is the attribute Mode'Enum_Rep (Fault), which yields 4, and Mode'Enum_Val (4) goes the other way. These started as GNAT-specific attributes and were added to the language in Ada 2022.
The route that works with any compiler is an unchecked conversion between the enumeration and an integer type of the same size. Fix the size first with for Mode'Size use 8;, then instantiate function To_Byte is new Ada.Unchecked_Conversion (Mode, Interfaces.Unsigned_8);. To_Byte (Fault) is then 4.
The two types must have the same size, otherwise the result is implementation-defined, and the compiler normally warns about the mismatch.
For the incoming direction the danger is an invalid pattern. If you unchecked-convert the byte 3 into a Mode, the object holds a value that is none of the three literals, and using it in a case statement or as an array index is erroneous.
Test it first with the 'Valid attribute: convert into a local variable M, then write if M'Valid then and report a protocol error in the else branch. 'Valid exists exactly for data arriving from outside the program, and it is the one thing you may safely do with a possibly invalid object. With Mode'Enum_Val, an unknown code raises Constraint_Error instead, which you can handle.
Consider whether you need the representation clause at all. A constant lookup table keeps the enumeration contiguous and needs no unchecked code: Code : constant array (Mode) of Interfaces.Unsigned_8 := (Idle => 1, Run => 2, Fault => 4);, with a case on the received byte for decoding, where the others branch handles invalid input.
Enumerations with gaps in their codes also cost a little at run time, because 'Pos, 'Succ, array indexing and for loops over the type have to translate between code and position. The clause is most useful when the type is a field of a record that is laid directly over a hardware register.
Back to Ada & SPARK community
