AdaCore Blog

19 entries tagged with #CodePeer

by Yannick Moy

Research Corner - Floating-Point Computations in SPARK

It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.

#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 Raphaël Amiard, Yannick Moy, Pierre-Marie de Rodat

Going After the Low Hanging Bug

At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).

#Static Analysis   

by Yannick Moy

New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs

​NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities"​ in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. Among formal methods, the report highlights strong suits of SPARK, and cites SPARK projects as example of mature uses of formal methods. NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie". So if your new year's resolutions include software without bugs, have a look at SPARK in 2017.

#VerificationTools    #Formal Methods    #SPARK   

by Johannes Kanig

SPARK and CodePeer, a Good Match!

It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!

#Formal Verification    #SPARK   

by Yannick Moy

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

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.

#Formal Verification    #SPARK   

by Emmanuel Briot

Integrate new tools in GPS

This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.

#GPS   

by AdaCore Admin

Certification and Qualification

AdaCore provides several tools with certification and qualification capabilities, for the rail and avionics industry. Quentin Ochem’s presentation on “Certification and Qualification” at the 2015 AdaCore Tech Days in Boston, Massachusetts provided more information about these two standards, namely DO-178C and EN:50128:2011.

#TechDay    #Certification    #CodePeer   

by AdaCore Admin

Provably safe programming at Embedded World

AdaCore continues to build reliable and secure software for embedded software development tools. Last month, we attended Embedded World 2016, one of the largest conferences of its kind in Europe, to present our embedded solutions and our expertise for safety, and mission critical applications in a variety of domains.

#ARM    #emb2016    #embedded    #Embedded World   

by Yannick Moy

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 AdaCore Admin

AdaCore Tech Days 2015

#AdaCoreTechDay    #GNAT Pro    #CodePeer    #SPARK Pro    #SPARK    #QGen   

by Yannick Moy

How Our Compiler Learnt From Our Analyzers

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.

#Compilation    #Formal Verification    #SPARK   

by Jamie Ayre

Verification on Ada code with Static and Dynamic Code Analysis - Webinar

One of the main challenges to get certification in Ada projects is the achievement of 100% code coverage but in most projects an amount of more than 95% structural coverage is hard to achieve. What can you do with the last 5% of code that can't be covered? DO-178C for example, provides a framework for the integration of various techniques in the development process to solve the problem. In this webinar you learn how static analysis and dynamic testing can help complete analysis for pieces of code that are not covered.

#CodePeer    #Code Coverage    #Dynamic Analysis    #Static Analysis    #DO-178    #DO-178C   

by Jamie Ayre

20 years on...

20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions

#20th Anniversary    #AdaLove   

by Olivier Ramonat

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0

February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.

#GNAT Pro    #SPARK Pro    #GPS    #GNATbench    #GNATdashboard    #Ada    #AdaCore Factory    #CodePeer    #QGen   

by Johannes Kanig

Testing, Static Analysis, and Formal Verification

I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).

#Formal Methods    #Static Analysis    #Testing   

by Johannes Kanig

SPARK 15: Errors, Warnings and Checks

The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the motivation behind it.

#Formal Verification    #SPARK   

by Yannick Moy

Studies of Contracts in Practice

Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts (Eiffel obviously, Java with JML contracts and C# with Code Contracts). I'm reporting what I found interesting (and less so) in these two studies.

#Language    #Formal Verification    #Contracts