test-ada: showcase Ada/SPARK object construction

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;

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;

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_ */

repos/libports/src/test/ada/spark.adc

@@ -0,0 +1,2 @@
+pragma SPARK_Mode (On);
+pragma Check_Policy (Debug, Disable);

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);
 }

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