GNUBoot
/
coreboot-kgpe-d16
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
coreboot-kgpe-d16/gnat.adc

31 lines
1.1 KiB
Plaintext
Raw Normal View History

treewide: more SPDX header work Change-Id: Ib78c322730ec6dfa9dcaafa16e5741cd3d351b8d Signed-off-by: Patrick Georgi <pgeorgi@google.com> Reviewed-on: https://review.coreboot.org/c/coreboot/+/41174 Tested-by: build bot (Jenkins) <no-reply@coreboot.org> Reviewed-by: Martin Roth <martinroth@google.com> Reviewed-by: HAOUAS Elyes <ehaouas@noos.fr>
2020-05-08 18:32:38 +02:00
-- SPDX-License-Identifier: GPL-2.0-only
Make Ada a first class citizen Some remarks on the make process: o We usually leave Ada specs (.ads files which are like c headers) together with the bodies (implementations in .adb files) in one directory. So we have to know, where they live. o If there is no matching .adb an .ads is a valid source file and we'll generate an object file from it. o Object files need to have the same basename as their source files :-/ That's why we put them in build/<class>/ dirs now. o We track dependencies by looking at the compiler output (.ali files which accompany every .o). This way we don't need any gnatmake magic, or even more complex, less portable tools. For ADAFLAGS_common, I simply copied the CFLAGS_common whilst dropping everything unsupported and adding sane warning options. The set of language features is highly restricted (see gnat.adc). This should suit the embedded nature of coreboot and helps proving absence of runtime errors with SPARK. Change-Id: I70df9adbd467ecd2dc7c5c1cf418b7765aca4e93 Signed-off-by: Nico Huber <nico.h@gmx.de> Reviewed-on: https://review.coreboot.org/13044 Tested-by: build bot (Jenkins) Reviewed-by: Stefan Reinauer <stefan.reinauer@coreboot.org> Reviewed-by: Edward O'Callaghan <edward.ocallaghan@koparo.com>
2016-01-14 01:13:33 +01:00
pragma Restrictions (No_Access_Subprograms);
pragma Restrictions (No_Allocators);
pragma Restrictions (No_Calendar);
pragma Restrictions (No_Dispatch);
pragma Restrictions (No_Exception_Handlers);
pragma Restrictions (No_Fixed_Point);
pragma Restrictions (No_Floating_Point);
pragma Restrictions (No_Implicit_Dynamic_Code);
pragma Restrictions (No_Implicit_Heap_Allocations);
pragma Restrictions (No_Implicit_Loops);
pragma Restrictions (No_Initialize_Scalars);
pragma Restrictions (No_IO);
pragma Restrictions (No_Local_Allocators);
pragma Restrictions (No_Recursion);
pragma Restrictions (No_Secondary_Stack);
pragma Restrictions (No_Streams);
pragma Restrictions (No_Tasking);
pragma Restrictions (No_Unchecked_Access);
pragma Restrictions (No_Unchecked_Deallocation);
pragma Restrictions (No_Wide_Characters);
pragma Restrictions (Static_Storage_Size);
pragma Assertion_Policy
(Statement_Assertions => Disable,
Pre => Disable,
gnat.adc: Do not generate assertion code for Refined_Post Ada usually does lots of type and contract checking during runtime. As this produces overhead and there is nobody to tell when we run into an exception, we disable code generation for those checks. Now disable it for `Refined_Post` too, which was just missed earlier. Change-Id: I67ca754f830e387efee3930e86929eb494bfaf03 Signed-off-by: Nico Huber <nico.huber@secunet.com> Reviewed-on: https://review.coreboot.org/16945 Tested-by: build bot (Jenkins) Reviewed-by: Martin Roth <martinroth@google.com>
2016-10-05 17:45:33 +02:00
Post => Disable,
Refined_Post => Disable);
Make Ada a first class citizen Some remarks on the make process: o We usually leave Ada specs (.ads files which are like c headers) together with the bodies (implementations in .adb files) in one directory. So we have to know, where they live. o If there is no matching .adb an .ads is a valid source file and we'll generate an object file from it. o Object files need to have the same basename as their source files :-/ That's why we put them in build/<class>/ dirs now. o We track dependencies by looking at the compiler output (.ali files which accompany every .o). This way we don't need any gnatmake magic, or even more complex, less portable tools. For ADAFLAGS_common, I simply copied the CFLAGS_common whilst dropping everything unsupported and adding sane warning options. The set of language features is highly restricted (see gnat.adc). This should suit the embedded nature of coreboot and helps proving absence of runtime errors with SPARK. Change-Id: I70df9adbd467ecd2dc7c5c1cf418b7765aca4e93 Signed-off-by: Nico Huber <nico.h@gmx.de> Reviewed-on: https://review.coreboot.org/13044 Tested-by: build bot (Jenkins) Reviewed-by: Stefan Reinauer <stefan.reinauer@coreboot.org> Reviewed-by: Edward O'Callaghan <edward.ocallaghan@koparo.com>
2016-01-14 01:13:33 +01:00
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
pragma SPARK_Mode (On);