AdaCore Blog

10 entries tagged with #refactoring

by Fabien Chouteau

Ada/SPARK Crate Of The Year 2022 Winners Announced!

In June of 2022 we launched the second edition of the 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 320 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,both inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.

by Roderick Chapman

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   

by Claire Dross

Relaxing the Data Initialization Policy of SPARK

SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like access types) or SPARK specific developments. However, new features generally take a while to make it into actual user code. The feature I am going to present here is in my experience an exception, as it was used both internally and by external users before it made it into any actual release. It was designed to enhance the verification of data initialization, whose limitations have been a long standing issue in SPARK.

#Formal Verification    #SPARK   

by Yannick Moy

(Many) More Low Hanging Bugs

We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.

#Static Analysis    #Libadalang   

by Yannick Moy , Nicolas Roche

A Usable Copy-Paste Detector in A Few Lines of Python

After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.

#Libadalang    #Static Analysis    #refactoring   

by Yannick Moy

VerifyThis Challenge in SPARK

This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.

#Formal Verification    #SPARK