by Yannick Moy , Lionel Matias

30 entries tagged with #CodePeer
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.
Part of our core expertise at AdaCore is to integrate multiple technologies as smoothly as possible and make it a product. This started at the very beginning of our company by integrating a code generator (GCC) with an Ada front-end (GNAT) which was then followed by integrating a debugger engine (GDB) and led to today's rich GNAT Pro offering.
Presenting the GNAT LLVM projectAt AdaCore labs, we have been working for some time now on combining the GNAT Ada front-end with a different code generator than GCC.
A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.
In Part 1 of this blog post I discussed why I chose to implement this application using the Ada Web Server to serve the computed fractal to a web browser. In this part I will discuss a bit more about the backend of the application, the Ada part.
The promise behind the SPARK language is the ability to formally demonstrate properties in your code regardless of the input values that are supplied - as long as those values satisfy specified constraints. As such, this is quite different from static analysis tools such as our CodePeer or the typical offering available for e.g. the C language, which trade completeness for efficiency in the name of pragmatism. Indeed, the problem they’re trying to solve - finding bugs in existing applications - makes it impossible to be complete. Or, if completeness is achieved, then it is at the cost of massive amount of uncertainties (“false alarms”). SPARK takes a different approach. It requires the programmer to stay within the boundaries of a (relatively large) Ada language subset and to annotate the source code with additional information - at the benefit of being able to be complete (or sound) in the verification of certain properties, and without inundating the programmer with false alarms.
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.
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.
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.
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.
20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions
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.
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).