AdaCore Blog

11 entries tagged with #Testing

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

Building High-Assurance Software without Breaking the Bank

AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.

#Formal Methods    #SPARK   

by Jérôme Lambourg

Efficient use of Simics for testing

As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.

#Simics    #WindRiver    #GNAT Pro   

by AdaCore Admin

VectorCAST/Ada: Ada 2012 Language Support

We are pleased to announce that on April 27th our partner, Vector, will host a webinar to showcase their latest VectorCAST/Ada release!

by Jerome Guitton, Jérôme Lambourg, Joel Brobecker

Simics helps run 60 000 GNAT Pro tests in 24 hours

A key aspect of AdaCore’s GNAT Pro offering is the quality of the product we’re delivering and our proactive approach to resolving issues when they appear. To do so, we need both intensive testing before delivering anything to our customers and to produce “wavefront” versions every day for each product we offer. Doing so each and every day is a real challenge, considering the number of supported configurations, the number of tests to run, and the limit of a 24-hour timeframe. At AdaCore, we rely heavily on virtualization as part of our testing strategy. In this article, we will describe the extent of our GNAT Pro testing on VxWorks, and how Simics helped us meet these challenges.

#Simics    #WindRiver    #GNAT Pro   

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

Formal Verification Made Easy!

We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.

#SPARK Pro    #SPARK2014     #SPARKPro16   

by Fabien Chouteau

Make with Ada: Formal proof on my wrist

When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.

#SPARK2014     #Smartwatch    #Makers   

by Emmanuel Briot

Traits-Based Containers

This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.

#Ada    #Containers    #Generics   

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