Skip to content
This repository has been archived by the owner on Aug 2, 2022. It is now read-only.

Componolit Ada Runtime 1.1.0

Compare
Choose a tag to compare
@jklmnn jklmnn released this 26 Jul 12:46
· 55 commits to master since this release

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