Enhancing Ada Embedded Development: The Power of Real-Time Logging with RTT

Efficient embedded development in Ada relies on powerful tools. Real-time logging plays a pivotal role, enabling live monitoring and analysis. Unlike traditional methods, SEGGER's Real-Time Transfer (RTT) method offers hardware-independent real-time logging with low latency.This article explores RTT's simplicity: storing protocol data in a ring buffer on the target device, read by the debugger without halting program execution. The provided Ada code showcases RTT's implementation, from buffer types to control blocks.Integration with development environments is seamless, as seen with the Cortex Debug extension for VS Code. The extension supports RTT, providing features like textual and graphical display of RTT stream data.In summary, SEGGER's RTT method is a powerful, hardware-independent solution for real-time logging in Ada development. Its efficiency and flexibility make it indispensable for debugging, error detection, and security in embedded systems. Explore the GitHub repository for a hands-on experience with RTT in Ada embedded development.

#Embedded    #DIY    #vscode   

Building a GNAT SAS analysis pipeline on GitLab

This is the first part of a series in which we’ll implement a GNAT SAS analysis pipeline for Ada code on GitLab by making use of GNAT SAS 24 new features. We are focusing on getting a pipeline that "Just Works(tm)", leaving more advanced issues such as scalability, improvement of user experience, or maintainability for later.

#Docker    #GitLab    #CodePeer    #DevOps    #GNAT SAS   

Memory Safety in Ada and SPARK through Language Features and Tool Support

This blog post describes how Ada and SPARK provide memory safety through a combination of language features, run-time checks, and static and dynamic analysis tools.

#memory safety    #safe programming languages    #Ada    #SPARK   

An Introduction to Memory Safety Concepts and Challenges

This blog post explains the concept of memory safety and the most common memory errors. Then, it introduces three memory-safe languages that have built-in countermeasures against memory errors.

#Programming     #memory safety    #memory bugs    #Ada    #SPARK    #Rust   

A little bit of Photoshop® using GNAT for CUDA®

Today I want to go over some internal mechanisms of a Photoshop-like application to better illustrate an up-and-coming tech, GNAT for CUDA®, developed at AdaCore.

#CUDA    #GNAT Pro    #Photoshop    #GPU    #Ada    #AdaCore    #NVIDIA    #GPGPU    #Computer Vision    #Image Analysis    #Bilateral Filter    #Signal Processing    #parallel computing    #Surface Blur    #Image Processing   

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   

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   

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   

Automated Assurance through Differential Fuzzing

This blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the results of a differential fuzzing campaign for the Libkeccak and XKCP cryptographic libraries.

#Fuzzing    #SPARK    #Testing    #Security   

Avoiding Vulnerabilities in Crypto Code with SPARK

Writing secure software in C is hard. It takes just one missed edge case to lead to a serious security vulnerability, and finding such edge cases is difficult. This blog post discusses a recent vulnerability in a popular SHA-3 library and how the same problems were avoided in my own SHA-3 library written in SPARK.

#Security    #SPARK    #Cryptography    #Formal Verification