AdaCore Blog

An Insight Into the AdaCore Ecosystem

by Yannick Moy –
Formal Verification of Legacy Code

Formal Verification of Legacy Code

Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.

#SPARK    #Legacy    #Formal Methods   

by Yannick Moy –

GNATprove Tips and Tricks: What’s Provable for Real?

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

#Formal Verification    #SPARK   

by Yannick Moy –

SPARK 2014 Rationale: Support for Ravenscar

As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.

#Language    #Formal Verification    #SPARK   

by David Hauzar –

SPARK 16: Generating Counterexamples for Failed Proofs

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

#Formal Verification    #SPARK   

by Yannick Moy –

GNATprove Tips and Tricks: User Profiles

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

#Formal Verification    #SPARK