[coreboot-gerrit] Patch set updated for coreboot: WIP: Dramatically increase Jenkins' CPU usage

[Nico Huber (nico.h@gmx.de)]

Nico Huber (nico.h at gmx.de) just uploaded a new patch set to gerrit, which you can find at https://review.coreboot.org/13121

-gerrit

commit ce53e95b1894376e7bdedae1b2a82c5e0c8a3525
Author: Nico Huber <nico.h at gmx.de>
Date:   Fri Jan 22 00:29:38 2016 +0100

    WIP: Dramatically increase Jenkins' CPU usage
    
    Change-Id: I35f14d9a27453b1f043d207deea017d5277bb8a6
    Signed-off-by: Nico Huber <nico.h at gmx.de>
---
 Makefile.inc   | 41 ++++++++++++++++++++++++++++++++++++++++-
 spark.adc      | 39 +++++++++++++++++++++++++++++++++++++++
 spark.gpr.tmpl | 26 ++++++++++++++++++++++++++
 3 files changed, 105 insertions(+), 1 deletion(-)

diff --git a/Makefile.inc b/Makefile.inc
index 6680561..7274141 100644
--- a/Makefile.inc
+++ b/Makefile.inc
@@ -47,7 +47,7 @@ export objgenerated := $(obj)/generated
 #######################################################################
 # root rule to resolve if in build mode (ie. configuration exists)
 real-target: $(obj)/config.h coreboot
-coreboot: build-dirs $(obj)/coreboot.rom $(obj)/cbfstool $(obj)/rmodtool
+coreboot: build-dirs $(obj)/coreboot.rom $(obj)/cbfstool $(obj)/rmodtool $(foreach stage,$(COREBOOT_STANDARD_STAGES),prove-$(stage))
 
 #######################################################################
 # our phony targets
@@ -376,6 +376,12 @@ CFLAGS_common += -Os
 ADAFLAGS_common += -Os
 endif
 
+PROOF_MODE_common ?= all
+SPARKFLAGS_common += \
+	--warnings=error --report=fail \
+	-j$(CPUS) -k -m --timeout=10 \
+	--mode=$(PROOF_MODE_common) \
+
 additional-dirs := $(objutil)/cbfstool $(objutil)/romcc $(objutil)/ifdtool \
 		   $(objutil)/ifdfake $(objutil)/options $(objutil)/amdfwtool \
 		   $(objutil)/cbootimage $(objutil)/bimgtool
@@ -971,3 +977,36 @@ what-jenkins-does:
 	util/abuild/abuild -B -J $(if $(JENKINS_NOCCACHE),,-y) -c $(CPUS) -z -p $(JENKINS_PAYLOAD)
 	(cd payloads/libpayload; unset COREBOOT_BUILD_DIR; $(MAKE) $(if $(JENKINS_NOCCACHE),,CONFIG_LP_CCACHE=y) V=$(V) Q=$(Q) junit.xml)
 	$(foreach tool, $(TOOLLIST), $(MAKE) CPUS=$(CPUS) V=$(V) Q=$(Q) UTIL="$(tool)" MFLAGS= MAKEFLAGS= junit.xml; )
+
+prove_stage_comma := ,
+prove_stage_empty :=
+prove_stage_space := $(prove_stage_empty) $(prove_stage_empty)
+
+define prove_stage
+# $1 stage
+
+prove_$(1)_dirs = \
+	$$(subst $$(prove_stage_space),$$(prove_stage_comma)$$(prove_stage_space),$$(patsubst %,"%", \
+		$$(abspath src/lib/debug/null/ $$(filter-out %/ada/,$$($(1)-ada-dirs)))))
+
+$(obj)/$(1)/spark.gpr: spark.gpr.tmpl
+	$$(if $$($(1)-ada-dirs), \
+	sed \
+		-e's|<<SOURCE_DIRS>>|$$(prove_$(1)_dirs)|' \
+		-e's|<<OBJECT_DIR>>|$(patsubst %,"%",$(absobj)/$(1))|' \
+		-e's|<<SPARK_ADC>>|$(patsubst %,"%",$(abspath $(top)/spark.adc))|' \
+		$$< >$$@ \
+	)
+
+$(obj)/$(1)/gnatprove/gnatprove.out: $(obj)/$(1)/spark.gpr $$($(1)-srcs) $$($(1)-extra-specs) src/lib/debug/null/hw-debug_sink.ads
+	$$(if $$($(1)-ada-dirs), \
+	gnatprove \
+		$$(SPARKFLAGS_common) $$(SPARKFLAGS_$(1)) -P$(absobj)/$(1)/spark \
+	)
+
+prove-$(1): $(obj)/$(1)/gnatprove/gnatprove.out
+
+endef
+
+$(foreach stage,$(COREBOOT_STANDARD_STAGES), \
+	$(eval $(call prove_stage,$(stage))))
diff --git a/spark.adc b/spark.adc
new file mode 100644
index 0000000..f0354c3
--- /dev/null
+++ b/spark.adc
@@ -0,0 +1,39 @@
+--
+-- 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_Enumeration_Maps);
+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
+  (Debug                => Disable);
+pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
+pragma SPARK_Mode (On);
diff --git a/spark.gpr.tmpl b/spark.gpr.tmpl
new file mode 100644
index 0000000..2315094
--- /dev/null
+++ b/spark.gpr.tmpl
@@ -0,0 +1,26 @@
+--
+-- 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.
+--
+
+library project SPARK is
+
+   for Library_Name use "spark";
+   for Library_Dir use <<OBJECT_DIR>> & "/adalib";
+
+   for Source_Dirs use (<<SOURCE_DIRS>>);
+   for Object_Dir use <<OBJECT_DIR>>;
+
+   package Builder is
+      for Global_Configuration_Pragmas use <<SPARK_ADC>>;
+   end Builder;
+
+end SPARK;