[coreboot-gerrit] [S] Change in libgfxinit[master]: dp info: Provide Link_Status'Object_Size and padding

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/68105 )

Change subject: dp info: Provide Link_Status'Object_Size and padding
......................................................................

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`.

Change-Id: Id7f6b9f50105d9357adcb60fd551b719d9eccd30
Signed-off-by: Nico Huber 
---
M common/hw-gfx-dp_info.adb
M common/hw-gfx-dp_info.ads
2 files changed, 23 insertions(+), 1 deletion(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/05/68105/1

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;

----------------------------------------------------------------------------