Namely, GNAT Pro, the Common Code Generator (CCG) and SPARK Pro completed the qualification process for automotive and industrial standards.
GNAT Pro is a robust and flexible development environment comprising an industrial-grade toolchain that supports the Ada and C programming languages, either standalone or mixed in a single binary. GNAT Pro comes with a range of development and verification tools, including stack size computation, coding standard verification, and a customisable/extensible IDE.
The Common Code Generator (CCG) compiles from a SPARK-like Ada subset to C code. CCG allows projects to cross-compile Ada and SPARK applications to any hardware target that provides a C compiler, including targets that do not come with off-the-shelf Ada support.
SPARK Pro is a toolset based on an Ada language subset that allows developers to formally guarantee properties of source code, such as the absence of certain categories of vulnerabilities (buffer overflow, division by zero, references to uninitialised variables), and to prove custom functional assertions.
Both the GNAT Pro compiler and CCG received TCL3 qualification under ISO 26262, and T3 qualification under IEC 61508. The SPARK Pro verification tool received TCL3 and T2 qualification. All three products have been certified by TÜV SÜD, an independent, globally recognised organisation which confirms that products meet national and international standards.
AdaCore – www.adacore.com