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);
diff --git a/common/hw-gfx-dp_info.ads b/common/hw-gfx-dp_info.ads
index 6d22bcc..732894b 100644
--- a/common/hw-gfx-dp_info.ads
+++ b/common/hw-gfx-dp_info.ads
@@ -63,16 +63,21 @@
type Adjust_Requests_Array is array (Lane_Index) of Adjust_Request;
pragma Pack (Adjust_Requests_Array);
+ type Link_Status_Padding is mod 2**15;
type Link_Status is record
Lanes : Lanes_Status;
Interlane_Align_Done : Boolean;
+ Padding : Link_Status_Padding;
Adjust_Requests : Adjust_Requests_Array;
end record;
for Link_Status use record
Lanes at 16#00# range 0 .. 15;
Interlane_Align_Done at 16#02# range 0 .. 0;
+ Padding at 16#02# range 1 .. 15;
Adjust_Requests at 16#04# range 0 .. 15;
end record;
+ for Link_Status'Size use 48;
+ for Link_Status'Object_Size use 48;
----------------------------------------------------------------------------