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 <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68108
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
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.");