GNAT GPL 2017 is out!
For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.
For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.
The RISC-V open instruction set is getting more and more news coverage these days. In particular since the release of the first RISC-V microcontroller from SiFive and the announcement of an Arduino board at the Maker Faire Bay Area 2017.
A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)
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.
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.
In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.
User friendly strings API In a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.
This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.
This post has been updated in March 2017 and was originally posted in March 2016.
Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
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).
AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.
There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.
Customizing build target switches In the first post in this series (Integrate new tools in GPS) we saw how to create new build targets in GPS to spawn external tools via a menu or toolbar button, and then display the output of that tool in its own console, as well as show error messages in the Locations view.
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.
One of the interesting aspects of developing software for a bare-board target is that displaying complex application-created information typically requires more than the target board can handle. Although some boards do have amazing graphics capabilities, in some cases you need to have the application on the target interact with applications on the host. This can be due to the existence of special applications that run only (or already) on the host, in particular.
GNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.
The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new release of GPS.
Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.
The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.
As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view, and how you can now use it as a TODO list.
I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!
I started this project more than a year ago. It was supposed to be the first Make with Ada project but it became the most challenging from both, the hardware and software side.
As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.
Dr Carl Brandon of Vermont Technical College and his team of students used SPARK and Ada to successfully launch a satellite into space in 2013 and it has continued to orbit the Earth ever since! At our AdaCore Tech Days in Boston last year Dr Brandon explained further.
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.
Embedded products are not stand alone, this allows them to have safety, mission critical and real-time requirements that they wouldn’t necessarily have otherwise. The embedded product line provides analyzable, verifiable, and certifiable software for both static and dynamic analysis tools.
Embedded World will see the latest release of QGen, the qualifiable and customisable code generator for Simulink® and Stateflow® models!
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.
A step by step tutorial to adapt the ARM runtime to new MCUs/boards.
Frederick Pothon of ACG Solutions has recently published a document entitled - Dissimilar tools: Use cases and impact on tool qualification level on the open-DO blog.
This short post describes an idiom that can be used to help maintain complex hierarchies of tagged types, when methods need to call the parent types methods.
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.
Through the adoption of GitHub we have taken our first step on the way to having a more collaborative and dynamic interaction with, both our users and open source technologies.
We are continuing to develop tools for use within projects that require reliable and secure embedded software for ARM. Our engineering team have been busy creating demos running on ARM technology, such as Tetris in SPARK on ARM Cortex M4.
The Ada 2012 standard introduced user-defined references. The main idea behind this is simplifying the access to elements in a container. But you can use them to control the life-circle of your persistent objects. Let's see how it could work.
We are excited to be sponsoring and exhibiting at the 2nd annual High Integrity Software conference, taking place on 5th November 2015 at The Royal Marriott Hotel in Bristol.
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.
If you're somewhat interested in formal methods applied to software, but you never had the chance to really look at it, now is the time! Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College have written a truly essential book for getting up to speed with formal verification using SPARK. I really love this book, and here are the aspects I love most:
I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.
July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?
A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with electromagnetic field. In this article I will experiment a solenoid engine using a hacked hard drive and a software controller on a STM32F4 .
The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.
Reference countingReference counting is a way to automatically reclaim unused memory. An element is automatically deallocated as soon as there are no more references to it in the program.
This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store type specific information, outside of the type itself.
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.
I recently joined AdaCore as a Technical Account Manager with an initial focus on the UK and Scandinavian regions, but for the last 12 months I've been busy working on the AdaCore University. The most recent addition to which is a course on Mixed Language Programming with Ada, and it includes lectures on the integration of Ada with C, C++ and Java. The course covers some advanced topics like mixed language object orientation, techniques for using Ada strong typing to combat known issue with C pointers and the pitfalls that are encountered when mixing native Ada code with Java at runtime. This course clearly demonstrates that Ada has strong support for integration with C, C++ and Java and it proves there are no technical barriers to its adoption in modern mixed language software systems.
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).
I was at Bruxelles on January 31st to present the components of GNAT GPL 2015 : SPARK 2014 and GNAT GPL for ARM bare-board. This is not unrelated to a previous blog entry on Tetris in SPARK on ARM Cortex M4, in particular I presented that Tetris demo (I brought some boards with me and despite the simple package, none were broken!). The slides contain technical details on the ravenscar profile (main principles), how to build a program for the stm32f4-discovery board and how to port the runtime. There are also less technical slides such as why we choose the stm32f4 board and photos of some graphical demos. As that could be useful to anyone interested in Ravenscar or in porting the runtime to other boards or other platforms, we've made the slides available here.
Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.