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>
diff --git a/ada/dynamic_mmio/hw-mmio_range.adb b/ada/dynamic_mmio/hw-mmio_range.adb
index 86c8d1b..bdb6ab1 100644
--- a/ada/dynamic_mmio/hw-mmio_range.adb
+++ b/ada/dynamic_mmio/hw-mmio_range.adb
@@ -19,9 +19,10 @@
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 @@
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 :=