[S] Change in libgfxinit[master]: gma: Shuffle warning justifications to support old and new tooling

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/68108 )

Change subject: gma: Shuffle warning justifications to support old and new tooling
......................................................................

gma: Shuffle warning justifications to support old and new tooling

We annotate a check message because the actual behaviour of Power_Up_VGA
depends on the platform we compile for. For the same reason we have to
justify a warning that the annotation may be spurious. SPARK rules state
that the annotation has to directly follow the subprogram's body. Appa-
rently that also accounts for the warning justification, so move it
above the subprogram body.

Change-Id: I8f879e73b3ea43de7e10532fba6a9b2bb9eecfcf
Signed-off-by: Nico Huber 
---
M common/hw-gfx-gma.adb
1 file changed, 19 insertions(+), 2 deletions(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/08/68108/1

diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 851686e..87c8fb0 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -606,6 +606,8 @@
    pragma Warnings
      (GNATprove, Off, """Registers.Register_State"" * is not modified*",
       Reason => "Power_Up_VGA is only effective in certain configurations.");
+   pragma Warnings
+     (GNATprove, Off, "no check message justified*", Reason => "see below");
    procedure Power_Up_VGA
    with
       Refined_Global =>
@@ -627,8 +629,6 @@
    begin
       Power_And_Clocks.Power_Up (Cur_Configs, Fake_Config);
    end Power_Up_VGA;
-   pragma Warnings
-     (GNATprove, Off, "no check message justified*", Reason => "see below");
    pragma Annotate
      (GNATprove, Intentional, "unused global",
       "Power_Up_VGA is only effective in certain configurations.");