tree 6cfd183b235df313729af7645bc9a04e41e67809
parent 066e52eeaa329d782ccee96265a6a351fc395bf1
author Nico Huber <nico.h@gmx.de> 1662289489 +0200
committer Nico Huber <nico.h@gmx.de> 1669654803 +0000

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>