Bare-metal C++ development environment for certifiable safety-critical applications

We are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting different subsets of the C++ language. It constitutes the best choice for safety-critical bare-metal systems that want to reduce complexity, memory footprint and execution-time overhead, paving the way to software certification. GNAT Pro for C++ targets popular hardware in the avionics, defense, railway, and space domains: PowerPC (32 bits), x86 (64 bits), RISC-V (32/64 bits), LEON3 (32 bits) and ARM (32/64 bits).

#C++    #Safety Critical Development    #Certification    #Bare-metal   

Identifying and authorizing users at AdaCore

Back in the 90s when AdaCore was founded, the state of IT security was very different. A unique Unix login and password were enough to connect to a shared server and run business applications. Most of the protocols used were still unencrypted, and the most elaborate access controls were based on Unix groups and perimeter defense. As the company evolved, we gave users access to more and more services, some not hosted on-premise. More services meant distinct credentials. Security-savvy users, who did not accept reusing the same password everywhere, had the burden of maintaining all these distinct credentials. Most credentials were long-lived, and very often shared. Also as the notion of perimeter defense became more and more fuzzy with the introduction of PaaS, IaaS, .. the need for safer access and communication protocols increased significantly.

#DevOps    #Security   

Extending Priority Inheritance Beyond Protected Operations

This blog entry shows how to define protected types that extend the language-defined priority inheritance for protected actions to the statements outside those protected actions. We create a mutex type for illustration.

#Ada    #Protected Types    #Priority Inheritance   

VSS: Cursors, Iterators and Markers

The VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing capa­bil­i­ties. It offers a con­ve­nient and robust API that allows devel­op­ers to work with Uni­code text, regard­less of its inter­nal rep­re­sen­ta­tion. Last time we provided overview of the library, and in this arti­cle, we will introduce concepts of cursors that are used to iterate, retrieve, and modify text data.

#vss    #Unicode    #strings    #Libraries   

SPARK, Beyond Normal Termination

When teaching SPARK to my students, I generally explain the central position of contracts in formal verification in the following way: Contracts of subprograms summarize their behavior - preconditions constrain their inputs, while postconditions describe their effects. It is an easy way to see contracts, However, not returning normally, for example looping forever or raising exceptions, is definitely a significant effect of a subprogram. Modeling that effect would be beneficial because if it occurs in an unexpected way it might cause the entire program to derail. Release 24.0 of SPARK includes contracts that can be used to reason about subprograms which do not return normally. This blog post describes them.

#SPARK    

Reducing Ada code bases with adareducer

How we're using Libadalang to create an automated Ada code reducer.

#Libadalang    #Ada   

Explainable Program Proofs

Ever wanted to understand why program proof is not as easy as telling ChatGPT "can you prove that program <code>stuff</code> is correct for me?" A new book from top-notch programmer and program proof expert Rustan Leino answers all your questions. Or at least a good batch.

#SPARK    #Formal Verification    #Programming     #Book   

The Case for SPARK Evolution - an April First Parable

SPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what about all the other cases? Should we put all our eggs in the same case? Discover what's cooking up for you on the side of language evolution.

#SPARK    #Dad Jokes   

Introduction to VSS library

The VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing capa­bil­i­ties. It offers a con­ve­nient and robust API that allows devel­op­ers to work with Uni­code text, regard­less of its inter­nal rep­re­sen­ta­tion. In this arti­cle, we will intro­duce you to the library and explain its pur­pose, high­light­ing its use­ful­ness for devel­op­ers work­ing in this area.

#Unicode    #strings    #Libraries    #vss