commit adfe11fec3f2fcca99be6b43bf4d33eb4aaf99d7
author Nico Huber <nico.h@gmx.de> Sun Jun 10 14:59:04 2018 +0200
committer Nico Huber <nico.h@gmx.de> Wed May 08 13:16:10 2019 +0000
tree 73275a1b5fe36a9a1a562c89dbf042c8e324a067
parent d9365613ea1dd31ae00bc69ebd2f7a508049b2c6

gma config: Make Config.CPU and Config.CPU_Var variable

Introduce CONFIG_GFX_GMA_DYN_CPU that, if set to `y`, makes `Config.CPU`
and `Config.CPU_Var` variables. All other config values derived from
these are turned into expression functions.

Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27068
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Reviewed-by: Patrick Georgi <pgeorgi@google.com>

common/hw-gfx-gma-registers.ads

diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index 3be2ec7..ac0f023 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -14,6 +14,7 @@
 
 with System;
 with HW.GFX.GMA;
+with HW.GFX.GMA.Config;
 
 private package HW.GFX.GMA.Registers
 with
@@ -1720,21 +1721,39 @@
 
    procedure Remove_Fence (First_Page, Last_Page : GTT_Range);
 
+   pragma Warnings (GNATprove, Off, "no check message justified by this",
+                    Reason => "see Annotate aspects.");
    procedure Write_GTT
      (GTT_Page       : GTT_Range;
       Device_Address : GTT_Address_Type;
       Valid          : Boolean)
    with
-      Global  => (In_Out => GTT_State),
-      Depends => (GTT_State =>+ (GTT_Page, Device_Address, Valid));
+      Global  =>
+        (Input => Config.Variable,
+         In_Out => GTT_State),
+      Depends =>
+        (GTT_State =>+ (Config.Variable, GTT_Page, Device_Address, Valid)),
+      Annotate =>
+        (GNATprove, Intentional,
+         """GMA.Config_State"" of ""Write_GTT"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    procedure Read_GTT
      (Device_Address :    out GTT_Address_Type;
       Valid          :    out Boolean;
       GTT_Page       : in     GTT_Range)
    with
-      Global  => (In_Out => GTT_State),
-      Depends => ((Device_Address, Valid, GTT_State) => (GTT_State, GTT_Page));
+      Global  =>
+        (Input => Config.Variable,
+         In_Out => GTT_State),
+      Depends =>
+        ((Device_Address, Valid, GTT_State) =>
+           (Config.Variable, GTT_State, GTT_Page)),
+      Annotate =>
+        (GNATprove, Intentional,
+         """GMA.Config_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");
 
    procedure Set_Register_Base (Base : Word64; GTT_Base : Word64 := 0)
    with