AdaCore Blog

5 entries tagged with #Code generation

SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.

#SPARK     #Cryptography    #Formal Verification    #Code generation    #RISC-V    #Security   

C library bindings: GCC plugins to the rescue

I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!

#Code generation    #Ada