Genode implements zero-footprint runtime for Ada and SPARK

Genode implements zero-footprint runtime for Ada and SPARK

[Ludovic Brenta]

Today on osnews.com's front page an innocuous phrase caught my
attention so I followed the links...

http://genode.org/documentation/release-notes/9.11#section-19

"At Genode Labs, we are exploring the use of the Spark subset of Ada
to implement security-critical code and use Genode as development
platform. For this reason, we have added support for executing
freestanding Ada code on Genode."

--
Ludovic Brenta.

Re: Genode implements zero-footprint runtime for Ada and SPARK

[Peter Hermann]

Ludovic Brenta <ludovic@ludovic-brenta.org> wrote:
> Today on osnews.com's front page an innocuous phrase caught my
> attention so I followed the links...

(-:
www.ihr.uni-stuttgart.de/forschung/ada/resources_on_ada/
:-)

thank you

Re: Genode implements zero-footprint runtime for Ada and SPARK

[AdaMagica]

Hm, later on this page it says "Elaboration is not performed". How can
then Ada code work at all?

Re: Genode implements zero-footprint runtime for Ada and SPARK

[Ludovic Brenta]

AdaMagica wrote on comp.lang.ada:
> Hm, later on this page it says "Elaboration is not performed". How can
> then Ada code work at all?

By restricting the compilation units in the program to only Pure and
Preelaborated units, I suppose.

--
Ludovic Brenta.

Re: Genode implements zero-footprint runtime for Ada and SPARK

[nfeske]

Hello,

as a developer of Genode, I am happy about the response to our Ada-
related
addition. As stated in the release notes, the current integration of
Ada
support is mainly geared towards using Genode as an experimentation
platform
for developing Spark sub programs. It is just the first step. If more
people
outside the current Genode developer community show interest in this
particular
topic, we will be happy to extend the Ada support as needed.

On Nov 26, 3:08 pm, AdaMagica <christoph.gr...@eurocopter.com> wrote:
> Hm, later on this page it says "Elaboration is not performed". How can
> then Ada code work at all?

The mentioned limitation refers to package initializations normally
performed
by the startup code generated by gnatbind, specifically the 'ada_init'
function.
The current use case for Ada on Genode is to use Spark for creating
type and
utility packages with free-standings functions called from C code.
Because such
packages have no internal state and no begin-end block, we can omit
gnatbind
for now. However, should the need for elaborating packages in the
right order
arise in the future, support for calling gnatbind will be added to the
build
environment. In short, the solution comes down to calling gnatmake
with the
'-c -b' arguments, adding the generated startup code to the program,
and
actually calling 'adainit'.

Best regards
Norman

please ignore

[Peter Hermann]

please ignore 123