dynamic_mmio: Use volatile access type

GCC 11 complains about an incompatible access type, e.g.

hw-pci-dev.adb:28:04: instantiation error at hw-mmio_range.adb:32
hw-pci-dev.adb:28:04: instantiation error at hw-pci-mmconf.adb:36
hw-pci-dev.adb:28:04: designated type and access type are not compatible with respect to volatility due to Async_Readers, Async_Writers, Effective_Reads, Effective_Writes

Declaring the access type volatile works around the issue, but we
have to also treat `Range_A` as external state now. Declaring it
as `Base_Address` state was an odd hack anyway.

To avoid further hassle, we also disable `SPARK_Mode`. Treating
this as SPARK code was never intended, and we use a shadow imple-
mentation (`proof/hw-mmio_range.adb`) for proofs anyway.

TEST=Doesn't affect coreboot binaries.

Change-Id: I9ddc8d1dafdcb41810e4c8bf29164ef7130def3f
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/c/libhwbase/+/55390
Reviewed-by: Jacob Garber <jgarber1@ualberta.ca>
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Reviewed-by: Patrick Georgi <pgeorgi@google.com>
Tested-by: Patrick Georgi <pgeorgi@google.com>
This commit is contained in:
Nico Huber 2021-06-10 16:36:31 +02:00 committed by Nico Huber
parent a3edc6ef32
commit fc2102f560
1 changed files with 4 additions and 3 deletions

View File

@ -19,9 +19,10 @@ with System.Address_To_Access_Conversions;
package body HW.MMIO_Range
with
SPARK_Mode => Off,
Refined_State =>
(State => null, -- the contents accessed, Range_A points to it
Base_Address => Range_A) -- the address, stored in Range_A
(State => Range_A, -- the contents accessed, Range_A points to it
Base_Address => null) -- the address, implicitly stored in Range_A
is
pragma Warnings (Off, "implicit dereference",
Reason => "This is what this package is about.");
@ -29,7 +30,7 @@ is
Debug_Reads : constant Boolean := False;
Debug_Writes : constant Boolean := False;
type Range_Access is access all Array_T;
type Range_Access is access all Array_T with Volatile;
package Conv_Range is new System.Address_To_Access_Conversions (Array_T);
Range_A : Range_Access :=