summaryrefslogtreecommitdiffstats
path: root/gnat.adc
diff options
context:
space:
mode:
authorNico Huber <nico.h@gmx.de>2016-01-14 01:13:33 +0100
committerNico Huber <nico.h@gmx.de>2016-09-19 11:14:18 +0200
commit2e09d2b239ff2dfdba89011fd64d9a07da0d8717 (patch)
tree74a3e2f4fd172232e81c2881ae1e3dfaae7bdf9a /gnat.adc
parentfec0328c5f653233859d4aec7dae0b94acb67e97 (diff)
downloadcoreboot-2e09d2b239ff2dfdba89011fd64d9a07da0d8717.tar.gz
coreboot-2e09d2b239ff2dfdba89011fd64d9a07da0d8717.tar.bz2
coreboot-2e09d2b239ff2dfdba89011fd64d9a07da0d8717.zip
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>
Diffstat (limited to 'gnat.adc')
-rw-r--r--gnat.adc40
1 files changed, 40 insertions, 0 deletions
diff --git a/gnat.adc b/gnat.adc
new file mode 100644
index 000000000000..3b463dc26a4f
--- /dev/null
+++ b/gnat.adc
@@ -0,0 +1,40 @@
+--
+-- This file is part of the coreboot project.
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+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,
+ Post => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);