scottk/OpenCellular
1
0
Fork 0
mirror of https://github.com/Telecominfraproject/OpenCellular.git synced 2026-01-17 02:21:15 +00:00
Code Issues Packages Projects Releases Wiki Activity

gma: Move a warning justification to spec

Browse Source 
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>
This commit is contained in:
Nico Huber
2017-06-12 23:04:46 +02:00
parent e015e82aff
commit bebca13b4d
2 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
common/hw-gfx-gma.adb
View File

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

3
common/hw-gfx-gma.ads
View File

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