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.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);