diff options
| author | Nico Huber <nico.huber@secunet.com> | 2024-02-19 15:02:55 +0100 |
|---|---|---|
| committer | Felix Held <felix-coreboot@felixheld.de> | 2024-03-01 18:46:30 +0000 |
| commit | ff2d863515334d3b90e03d4cf62c9a6c90df7ed0 (patch) | |
| tree | 76afb1188c0291405a1b334c6503221eb26c7227 | |
| parent | 0ada3dafd0d20c2a5b361237d7e9aabf8ed96457 (diff) | |
drivers/intel/gma: Allow SPARK function with side effects
Explicitly specifying the aspect `Side_Effects' is necessary for GCC
toolchains from 14.0 on. As older toolchains don't know the aspect,
we have to silence a warning about it, though.
Change-Id: I1eb879f57437587dc11d879fcc4042a70d384786
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/c/coreboot/+/80616
Reviewed-by: Felix Singer <service+coreboot-gerrit@felixsinger.de>
Reviewed-by: Thomas Heijligen <src@posteo.de>
Tested-by: build bot (Jenkins) <no-reply@coreboot.org>
| -rw-r--r-- | gnat.adc | 4 | ||||
| -rw-r--r-- | src/drivers/intel/gma/gma.ads | 2 |
2 files changed, 5 insertions, 1 deletions
@@ -28,3 +28,7 @@ pragma Assertion_Policy Refined_Post => Disable); pragma Overflow_Mode (General => Strict, Assertions => Eliminated); pragma SPARK_Mode (On); + +pragma Warnings + (GNAT, Off, """Side_Effects"" is not a valid aspect identifier", + Reason => """Side_Effects"" is new and needed for toolchain transition."); diff --git a/src/drivers/intel/gma/gma.ads b/src/drivers/intel/gma/gma.ads index d264960d2b..5cb45da8e7 100644 --- a/src/drivers/intel/gma/gma.ads +++ b/src/drivers/intel/gma/gma.ads @@ -11,6 +11,6 @@ package GMA is port : in Interfaces.C.int) return Interfaces.C.int with - Export, Convention => C, External_Name => "gma_read_edid"; + Side_Effects, Export, Convention => C, External_Name => "gma_read_edid"; end GMA; |