Language Support
AdaCore’s offerings are geared towards developers of embedded and native applications that demand high levels of assurance. Such software is written in a variety of programming languages, which AdaCore supports through compilers, multi-language build tools, IDEs, debuggers, and static and dynamic analysis tools.
Ada
The Ada language has a long and successful history in high-assurance systems on both native and embedded platforms, combining reliability, maintainability and performance. AdaCore has been at the forefront of advanced Ada technology since the company’s inception, and our products support all versions of the language standard: Ada 83, Ada 95, Ada 2005, and Ada 2012.
Products
Learn
SPARK
SPARK is an Ada 2012 subset that supports formal proofs of program properties ranging from absence of run-time errors to functional correctness (compliance of the code with formally specified requirements). As such the language is appropriate for applications at the highest levels of safety and/or security. SPARK can be integrated with code in other languages, such as Ada, C, or C++, using hybrid verification that combines formal methods with traditional testing-based approaches.
Products
Learn
C and C++
C remains the most common high-order language for embedded systems development, and in large applications C++ can bring the benefits of more powerful and expressive features while retaining C’s performance advantages. AdaCore’s gcc-based multi-language technology implements both C and C++, allowing programmers to develop software in either or both of these languages and, if applicable, integrate their code with Ada. AdaCore toolsets support C89 through C11 and C++89 through C++14.
Products
Simulink®
The Simulink® graphical modeling language, developed by The MathWorks, Inc., is particularly suited for designing control loops and dynamic systems. A Simulink® model is generally converted into an executable program on an embedded target processor in two steps: a code generator translates the model into source code in some programming language, and a compiler then compiles the source code into an executable. Oriented towards applications with safety certification requirements, AdaCore’s QGen toolsuite supports code generation to Ada (in fact SPARK) and to MISRA-C from a safe subset of Simulink® models. QGen supports Simulink® versions 2009b through 2017b.
Products
Other Languages
Ada, SPARK, C, C++ and Simulink® are supported by the core tools, but applications are not restricted to just these languages. Several tools provide either direct interfacing to other specific languages, for example Java and Python, or indirect interfacing through a compatibility layer in C.