gma: Move a warning justification to spec
Makes us compatible with SPARK 2017.
Change-Id: Ie325b913e329ceb522a320c76f1cccf512e5b79f
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/20170
Reviewed-by: Paul Menzel <paulepanter@users.sourceforge.net>
Reviewed-by: Patrick Georgi <pgeorgi@google.com>
Reviewed-by: Adrian-Ken Rueegsegger <ken@codelabs.ch>
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 101de18..a17a1ac 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -340,9 +340,6 @@
when Ironlake => Audio_VID_DID = 16#0000_0000#);
end Check_Platform;
begin
- pragma Warnings (GNATprove, Off, "unused variable ""Write_Delay""",
- Reason => "Write_Delay is used for debugging only");
-
pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
pragma Debug (Debug.Set_Register_Write_Delay (Write_Delay));
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 8285dcb..75dde9e 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -61,6 +61,8 @@
-- Only valid on primary pipe.
VGA_PLANE_FRAMEBUFFER_OFFSET : constant := 16#ffff_ffff#;
+ pragma Warnings (GNATprove, Off, "unused variable ""Write_Delay""",
+ Reason => "Write_Delay is used for debugging only");
procedure Initialize
(Write_Delay : in Word64 := 0;
Clean_State : in Boolean := False;
@@ -74,6 +76,7 @@
function Is_Initialized return Boolean
with
Global => (Input => Init_State);
+ pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
procedure Update_Outputs (Configs : Pipe_Configs);