tree f128acb526ae48ba8004919ce4e2c5a0785a0e1f
parent 3c1ac1884c3cbb64a95947f4f7f732ed1ce97169
author Nico Huber <nico.h@gmx.de> 1662291362 +0200
committer Nico Huber <nico.h@gmx.de> 1669655002 +0000

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>