Skip to content

Commit ff2d863

Browse files
n-huberfelixheld
authored andcommitted
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 <[email protected]> Reviewed-on: https://review.coreboot.org/c/coreboot/+/80616 Reviewed-by: Felix Singer <[email protected]> Reviewed-by: Thomas Heijligen <[email protected]> Tested-by: build bot (Jenkins) <[email protected]>
1 parent 0ada3da commit ff2d863

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

gnat.adc

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,7 @@ pragma Assertion_Policy
2828
Refined_Post => Disable);
2929
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
3030
pragma SPARK_Mode (On);
31+
32+
pragma Warnings
33+
(GNAT, Off, """Side_Effects"" is not a valid aspect identifier",
34+
Reason => """Side_Effects"" is new and needed for toolchain transition.");

src/drivers/intel/gma/gma.ads

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@ package GMA is
1111
port : in Interfaces.C.int)
1212
return Interfaces.C.int
1313
with
14-
Export, Convention => C, External_Name => "gma_read_edid";
14+
Side_Effects, Export, Convention => C, External_Name => "gma_read_edid";
1515

1616
end GMA;

0 commit comments

Comments
 (0)