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>
This commit is contained in:
parent
0ada3dafd0
commit
ff2d863515
4
gnat.adc
4
gnat.adc
@ -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.");
|
||||
|
@ -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;
|
||||
|
Loading…
x
Reference in New Issue
Block a user