5ccae43552
The minimal-footprint Ada runtime for implementing library-like functionality in SPARK is now called "spark" runtime. The full Ada runtime for entire components written in Ada and using the libc as glue to the underlying system will move to the world repository as "ada" runtime. Issue #3144
61 lines
1.1 KiB
C++
61 lines
1.1 KiB
C++
/*
|
|
* \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_ */
|