From 36934fbde04193046309dca1d8d3d27132d23882 Mon Sep 17 00:00:00 2001
From: Nico Huber <nico.h@gmx.de>
Date: Thu, 13 Jul 2017 00:08:21 +0200
Subject: [PATCH] Add `debug.adc` and option DEBUG

The GNAT configuration file `debug.adc` has Assertion_Policy Debug
enabled to compile `pragma Debug` code. If `DEBUG` is set to `1`
during build, `debug.adc` is used instead of the default `gnat.adc`.

Change-Id: If5b52f5251cae7deed7aca2765f9b5db1c148fb7
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/20558
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
---
 Makefile  | 10 ++++++++--
 debug.adc | 24 ++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 debug.adc

diff --git a/Makefile b/Makefile
index 91ef025..09881e5 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ libhw-dir := $(dir $(lastword $(MAKEFILE_LIST)))
 DESTDIR ?= dest
 
 name ?= hw
-hw-install = Makefile Makefile.proof gnat.adc spark.adc
+hw-install = Makefile Makefile.proof debug.adc gnat.adc spark.adc
 
 top := $(CURDIR)
 cnf := .config
@@ -34,6 +34,12 @@ $(foreach dep,$($(name)-deplibs), \
 
 include $(libhw-dir)/Makefile.proof
 
+ifeq ($(DEBUG),1)
+gnat-adc = $(libhw-dir)/debug.adc
+else
+gnat-adc = $(libhw-dir)/gnat.adc
+endif
+
 CC       = $(CROSS_COMPILE)gcc
 GNATBIND = $(CROSS_COMPILE)gnatbind
 
@@ -43,7 +49,7 @@ CFLAGS += -Wstrict-aliasing -Wshadow
 CFLAGS += -fno-common -fomit-frame-pointer
 CFLAGS += -ffunction-sections -fdata-sections
 
-ADAFLAGS += $(CFLAGS) -gnatA -gnatec=$(libhw-dir)/gnat.adc -gnatp
+ADAFLAGS += $(CFLAGS) -gnatA -gnatec=$(gnat-adc) -gnatp
 # Ada warning options:
 #
 #  a   Activate most optional warnings.
diff --git a/debug.adc b/debug.adc
new file mode 100644
index 0000000..536a5a3
--- /dev/null
+++ b/debug.adc
@@ -0,0 +1,24 @@
+pragma Restrictions (No_Allocators);
+pragma Restrictions (No_Calendar);
+pragma Restrictions (No_Dispatch);
+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_Local_Allocators);
+pragma Restrictions (No_Recursion);
+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,
+   Debug                => Check,
+   Pre                  => Disable,
+   Post                 => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);