From 41d10cff79435492d4a80deebb8e1b3020f25108 Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Fri, 1 Jun 2018 16:15:24 -0400
Subject: [PATCH] Add a SPARK Main template

---
 resources/templates/spark_main/example.yaml |  3 +++
 resources/templates/spark_main/main.adb     |  4 ++++
 resources/templates/spark_main/main.adc     |  6 ++++++
 resources/templates/spark_main/main.gpr     | 15 +++++++++++++++
 4 files changed, 28 insertions(+)
 create mode 100644 resources/templates/spark_main/example.yaml
 create mode 100644 resources/templates/spark_main/main.adb
 create mode 100644 resources/templates/spark_main/main.adc
 create mode 100644 resources/templates/spark_main/main.gpr

diff --git a/resources/templates/spark_main/example.yaml b/resources/templates/spark_main/example.yaml
new file mode 100644
index 0000000..5cc4d4d
--- /dev/null
+++ b/resources/templates/spark_main/example.yaml
@@ -0,0 +1,3 @@
+name: SPARK Main
+description: Simple overrideable provable main
+main: main
diff --git a/resources/templates/spark_main/main.adb b/resources/templates/spark_main/main.adb
new file mode 100644
index 0000000..e0d8401
--- /dev/null
+++ b/resources/templates/spark_main/main.adb
@@ -0,0 +1,4 @@
+procedure Main is
+begin
+   null;
+end Main;
diff --git a/resources/templates/spark_main/main.adc b/resources/templates/spark_main/main.adc
new file mode 100644
index 0000000..6a07ed7
--- /dev/null
+++ b/resources/templates/spark_main/main.adc
@@ -0,0 +1,6 @@
+
+pragma Profile(GNAT_Extended_Ravenscar);
+pragma Partition_Elaboration_Policy(Sequential);
+pragma SPARK_Mode (On);
+pragma Warnings (Off, "no Global contract available");
+pragma Warnings (Off, "subprogram * has no effect");
diff --git a/resources/templates/spark_main/main.gpr b/resources/templates/spark_main/main.gpr
new file mode 100644
index 0000000..7e52d62
--- /dev/null
+++ b/resources/templates/spark_main/main.gpr
@@ -0,0 +1,15 @@
+project Main is
+
+   for Main use ("main.adb");
+
+   package Compiler is
+      for Switches ("ada") use ("-g", "-gnatwa", "-gnatQ");
+   end Compiler;
+
+   package Builder is
+      for Switches ("ada") use ("-g", "-O0");
+
+      for Global_Configuration_Pragmas use "main.adc";
+   end Builder;
+
+end Main;