SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

How Our Compiler Learnt From Our Analyzers

by Yannick Moy in Compilation, Formal Verification – May 22, 2015

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.

A quick glimpse at the translation of Ada integer types in GNATprove

by Claire Dross in Formal Verification – April 15, 2015

In SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a library for bitvectors. Since bitwise operations can only be done on modular types in Ada, we currently translate arithmetic operations on signed integer types as operations on mathematical integers and arithmetic operations on modular types as operation on bitvectors. The only remaining question now is, how do we encode specific bounds of the Ada types into our Why3 translation ? In this post, I will present three different ways we tried to do this and explain which one we currently use and why.

Pardon my French: Test et Méthodes Formelles

by Yannick Moy in Events – April 1, 2015

After following for two years the very interesting French conference "Forum Méthodes Formelles", I am now part of the program committee, so will report on interesting topics to SPARK users. The next one is on test and formal methods.

GNATprove Tips and Tricks: Bitwise Operations

by Clément Fumex in Formal Verification – March 16, 2015

The ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations. We present some examples in this post.

GNATprove Tips and Tricks: Catching Mistakes in Contracts

by Yannick Moy in Formal Verification – February 18, 2015

Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.