tree 0e4428ad10de82b614fbe399f61fd1b6be5c6350
parent a3edc6ef32d09c566b7ea3555bc753458ec63039
author Nico Huber <nico.huber@secunet.com> 1623335791 +0200
committer Nico Huber <nico.h@gmx.de> 1623615035 +0000

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>