Componolit Ada Runtime 1.2.0

The Componolit Ada Runtime targets embedded devices and adds experimental support for two different ARM micro controllers and the ESP8266.

New features:

• Tagged type support (experimental)
• STM32F051 support (experimental)
• nRF52832 support (experimental)
• ESP8266 support (experimental)

Fixes:

• Missing weak symbols on Genode
• Reduce different log procedures to a single one

Componolit Ada Runtime 1.1.0

The Componolit Ada Runtime 1.1.0 adds support for Muen, increases the proof coverage and cleans up/removes deprecated features.

The following features have been added:

• Muen support
• Inline assembly support
• Can be built with pragma Restrictions (No_Exceptions)
• Proof of 64bit arithmetics with overflow check (addition and subtraction)
• Use of SPARK mode where possible

The following cleanups have been done:

• Removed GNAT.IO
• Separated the runtime linker interface from GNATs linker interface
• Replaced the custom secondary stack backing store with the Binders own mechanism

Componolit Ada Runtime 1.0.0

The Componolit Ada Runtime 1.0.0 builds upon GCC 8.3 and is compatible with GNAT Community 2019. It provides the following runtime features:

• Interfaces (C)
• Secondary stack
• Exception raising
• 64bit arithmetics
• Unchecked conversion

The following features are DEPRECATED and will be removed in future releases:

• GNAT IO

Parts of the runtime are proven to have no runtime errors:

• Secondary stack allocator
• String handling

Supported platforms:

• Genode
• Linux