From 98182379188fab9f262a8df8623d9fa4843a0ddc Mon Sep 17 00:00:00 2001
From: Norman Feske <norman.feske@genode-labs.com>
Date: Tue, 18 Dec 2018 16:47:17 +0100
Subject: [PATCH] test-ada: showcase Ada/SPARK object construction

---
 repos/libports/src/test/ada/machinery.adb | 20 ++++++++
 repos/libports/src/test/ada/machinery.ads | 30 ++++++++++++
 repos/libports/src/test/ada/machinery.h   | 60 +++++++++++++++++++++++
 repos/libports/src/test/ada/spark.adc     |  2 +
 repos/libports/src/test/ada/startup.cc    |  5 ++
 repos/libports/src/test/ada/target.mk     |  8 ++-
 6 files changed, 124 insertions(+), 1 deletion(-)
 create mode 100644 repos/libports/src/test/ada/machinery.adb
 create mode 100644 repos/libports/src/test/ada/machinery.ads
 create mode 100644 repos/libports/src/test/ada/machinery.h
 create mode 100644 repos/libports/src/test/ada/spark.adc

diff --git a/repos/libports/src/test/ada/machinery.adb b/repos/libports/src/test/ada/machinery.adb
new file mode 100644
index 0000000000..23a3e4795f
--- /dev/null
+++ b/repos/libports/src/test/ada/machinery.adb
@@ -0,0 +1,20 @@
+pragma Ada_2012;
+
+package body Machinery is
+
+   procedure Initialize (Machinery : out Machinery_Type) is
+   begin
+      Machinery := ( Temperature => 25 );
+   end Initialize;
+
+   function Temperature (Machinery : Machinery_Type) return Temperature_Type is
+   begin
+      return Machinery.Temperature;
+   end Temperature;
+
+   procedure Heat_Up (Machinery : in out Machinery_Type) is
+   begin
+      Machinery.Temperature := 77;
+   end Heat_Up;
+
+end Machinery;
diff --git a/repos/libports/src/test/ada/machinery.ads b/repos/libports/src/test/ada/machinery.ads
new file mode 100644
index 0000000000..947ed05397
--- /dev/null
+++ b/repos/libports/src/test/ada/machinery.ads
@@ -0,0 +1,30 @@
+package Machinery is
+
+   pragma Pure;
+
+   type Temperature_Type is mod 2**32 with Size => 32;
+
+   type Machinery_Type is private;
+
+   procedure Initialize (Machinery : out Machinery_Type)
+     with Export,
+          Convention    => C,
+          External_Name => "_ZN5Spark9MachineryC1Ev";
+
+   function Temperature (Machinery : Machinery_Type) return Temperature_Type
+     with Export,
+          Convention    => C,
+          External_Name => "_ZNK5Spark9Machinery11temperatureEv";
+
+   procedure Heat_up (Machinery : in out Machinery_Type)
+     with Export,
+          Convention    => C,
+          External_Name => "_ZN5Spark9Machinery7heat_upEv";
+
+private
+
+   type Machinery_Type is record
+      Temperature : Temperature_Type;
+   end record with Size => 32;
+
+end Machinery;
diff --git a/repos/libports/src/test/ada/machinery.h b/repos/libports/src/test/ada/machinery.h
new file mode 100644
index 0000000000..b1c79dcc15
--- /dev/null
+++ b/repos/libports/src/test/ada/machinery.h
@@ -0,0 +1,60 @@
+/*
+ * \brief  Example of implementing an object in Ada/SPARK
+ * \author Norman Feske
+ * \date   2018-12-18
+ */
+
+#ifndef _MACHINERY_H_
+#define _MACHINERY_H_
+
+/* Genode includes */
+#include <base/log.h>
+
+namespace Spark {
+
+	/**
+	 * Opaque object that contains the space needed to store a SPARK record.
+	 *
+	 * \param BYTES  size of the SPARK record in bytes
+	 */
+	template <Genode::size_t BYTES>
+	struct Object
+	{
+		long _space[(BYTES + sizeof(long) - 1)/sizeof(long)] { };
+	};
+
+	struct Machinery : Object<4>
+	{
+		Machinery();
+
+		void heat_up();
+
+		Genode::uint32_t temperature() const;
+	};
+}
+
+
+static inline void test_spark_object_construction()
+{
+	using namespace Genode;
+
+	Spark::Machinery machinery { };
+
+	auto check = [&] (char const *msg, Genode::uint32_t expected)
+	{
+		Genode::uint32_t const value = machinery.temperature();
+		log("machinery temperature ", msg, " is ", value);
+
+		class Spark_object_construction_failed { };
+		if (value != expected)
+			throw Spark_object_construction_failed();
+	};
+
+	check("after construction", 25);
+
+	machinery.heat_up();
+
+	check("after heating up", 77);
+}
+
+#endif /* _MACHINERY_H_ */
diff --git a/repos/libports/src/test/ada/spark.adc b/repos/libports/src/test/ada/spark.adc
new file mode 100644
index 0000000000..c1f72d5b92
--- /dev/null
+++ b/repos/libports/src/test/ada/spark.adc
@@ -0,0 +1,2 @@
+pragma SPARK_Mode (On);
+pragma Check_Policy (Debug, Disable);
diff --git a/repos/libports/src/test/ada/startup.cc b/repos/libports/src/test/ada/startup.cc
index a0ba8e43a0..81210fd26b 100644
--- a/repos/libports/src/test/ada/startup.cc
+++ b/repos/libports/src/test/ada/startup.cc
@@ -8,6 +8,9 @@
 #include <base/log.h>
 #include <base/component.h>
 
+/* local includes */
+#include <machinery.h>
+
 /**
  * Declaration of the Ada main procedure
  */
@@ -38,5 +41,7 @@ void Component::construct(Genode::Env &env)
 {
 	_ada_main();
 
+	test_spark_object_construction();
+
 	env.parent().exit(0);
 }
diff --git a/repos/libports/src/test/ada/target.mk b/repos/libports/src/test/ada/target.mk
index 4d846a5113..0dcc8da53c 100644
--- a/repos/libports/src/test/ada/target.mk
+++ b/repos/libports/src/test/ada/target.mk
@@ -1,4 +1,10 @@
 TARGET   = test-ada
-SRC_ADB  = main.adb
+SRC_ADB  = main.adb machinery.adb
 SRC_CC   = print.cc startup.cc
 LIBS     = base ada test-ada
+
+CC_ADA_OPT += -gnatec=$(PRG_DIR)/spark.adc
+
+INC_DIR += $(PRG_DIR)
+
+machinery.o : machinery.ads