dp info: Provide Link_Status'Object_Size and padding
We convert a plane byte buffer to a `Link_Status` object via an
`Unchecked_Conversion`. While the situation is actually clear
to the compiler because of the record representation clause for
`Link_Status`, SPARK rules demand an explicit `'Object_Size`.
The `'Object_Size` attribute specifies the exact size the
compiler should allocate for objects of the given type. The
`Padding` field is added to fill the gap left by reserved
bits.
Change-Id: Id7f6b9f50105d9357adcb60fd551b719d9eccd30
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68105
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/common/hw-gfx-dp_info.adb b/common/hw-gfx-dp_info.adb
index 392fee1..74e77a2 100644
--- a/common/hw-gfx-dp_info.adb
+++ b/common/hw-gfx-dp_info.adb
@@ -356,7 +356,9 @@
Success : out Boolean)
is
subtype Status_Index is DP_Defs.Aux_Payload_Index range 0 .. 5;
- subtype Status_Buffer is Buffer (Status_Index);
+ subtype Status_Buffer is Buffer (Status_Index)
+ with
+ Object_Size => 48;
function Buffer_As_Status is new Ada.Unchecked_Conversion
(Source => Status_Buffer, Target => Link_Status);