From bebca13b4d5eb4a3458ee63218fed05ca8ddf6aa Mon Sep 17 00:00:00 2001 From: Nico Huber Date: Mon, 12 Jun 2017 23:04:46 +0200 Subject: [PATCH] gma: Move a warning justification to spec Makes us compatible with SPARK 2017. Change-Id: Ie325b913e329ceb522a320c76f1cccf512e5b79f Signed-off-by: Nico Huber Reviewed-on: https://review.coreboot.org/20170 Reviewed-by: Paul Menzel Reviewed-by: Patrick Georgi Reviewed-by: Adrian-Ken Rueegsegger --- common/hw-gfx-gma.adb | 3 --- common/hw-gfx-gma.ads | 3 +++ 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb index 101de1807c..a17a1ace4a 100644 --- a/common/hw-gfx-gma.adb +++ b/common/hw-gfx-gma.adb @@ -340,9 +340,6 @@ is 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 8285dcbfad..75dde9ef26 100644 --- a/common/hw-gfx-gma.ads +++ b/common/hw-gfx-gma.ads @@ -61,6 +61,8 @@ is -- 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 @@ is function Is_Initialized return Boolean with Global => (Input => Init_State); + pragma Warnings (GNATprove, On, "unused variable ""Write_Delay"""); procedure Update_Outputs (Configs : Pipe_Configs);