14 entries tagged with #Unbound
by Manuel Hatzl
SPARK Crate of the Year: Unbounded containers in SPARKManuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/SPARK and how he created the spark_unbound library
by Fabien Chouteau
Ada/SPARK Crate Of The Year 2021 Winners Announced!
In June of 2021 we announced the launch of a new programming competition called Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 200 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
by Arnaud Charlet
Ada 202x support in GNAT
News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!
by Pat Rogers
From Ada to Platinum SPARK: A Case Study for Reusable Bounded StacksThis blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.
by Joffrey Huguet , Johannes Kanig
Proving a simple program doing I/O ... with SPARKThe functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip, which might process untrusted data downloaded from the internet, but also any servers that are directly connected to the internet, such as webservers, DNS servers and so on. In this blog post we show an approach that deals with error handling and reasoning about content, and demonstrate the approach using the cat command line utility.
by Johannes Kanig
Taking on a Challenge in SPARK
Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.
by Lionel Matias
Leveraging Ada Run-Time Checks with Fuzz Testing in AFLFuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code.Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide.Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.
by Pierre-Marie de Rodat
Pretty-Printing Ada Containers with GDB Scripts
When things don’t work as expected, developers usually do one of two things: either add debug prints to their programs, or run their programs under a debugger. Today we’ll focus on the latter activity.
by Emmanuel Briot
User-friendly strings API
User friendly strings APIIn a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.