gma: Merge `Config_State` into `State`
Treating `Config_State` separately was merely cosmetic and caused
lots of trouble. Its usage depends heavily on the selected plat-
form. Hence, `Global` contracts were not stable across different
configurations.
Let's avoid the annotation mess that it brought us and merge it
into `State`.
Change-Id: Ie28ccfc7ffbe08e0b3fe343d9e6df2420611834e
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35713
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index e9c8ab4..81fb219 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -1763,7 +1763,7 @@
(GTT_State =>+ (Config.Variable, GTT_Page, Device_Address, Valid)),
Annotate =>
(GNATprove, Intentional,
- """GMA.Config_State"" of ""Write_GTT"" not read",
+ """GMA.State"" of ""Write_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
procedure Read_GTT
@@ -1779,7 +1779,7 @@
(Config.Variable, GTT_State, GTT_Page)),
Annotate =>
(GNATprove, Intentional,
- """GMA.Config_State"" of ""Read_GTT"" not read",
+ """GMA.State"" of ""Read_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
pragma Warnings (GNATprove, On, "no check message justified by this");