AdaCore Blog

The Power of Technology Integration and Open Source

by Arnaud Charlet

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.

Today we are going much further in this area and I am going to give you a few concrete examples in this post.

For example take our advanced static analysis engine CodePeer and let's look at it from two different angles (a bit like bottom-up and top-down if you will): what does it integrate, and what other products integrate it?

From the first perspective, CodePeer integrates many different and complex pieces of technology: the GNAT front-end, various "core" GNAT tools (including GNATmetric, GNATcheck, GNATpp), the AdaCore IDEs (GNAT Studio, GNATbench), GNATdashboard, a Jenkins plug-in, GPRbuild, as well as the codepeer engine itself and finally as of version 20, libadalang and light checkers based on libadalang (aka "LAL checkers").

Thanks to this complex integration, CodePeer users can launch various tools automatically and get findings stored in a common database, and get a common user interface to drive it. Indeed, from CodePeer you can get access to: GNAT warnings, GNATcheck messages, LAL checkers, CodePeer "advanced static analysis" messages.

And the list will continue growing in the future, but that's for another set of posts!

Now from the other perspective, the codepeer engine is also integrated as an additional prover in our SPARK Pro product, to complement the SMT solvers integrated in SPARK, and is also used in our QGen product as the back-end of the QGen Verifier which performs static analysis on Simulink models.

Speaking of SPARK, this is also another good example of complex integration of many different technologies: the GNAT front-end, GPRbuild, GNAT Studio and GNATbench, GNATdashboard, Why3, CVC4, Z3, Alt-Ergo, the codepeer engine, and the SPARK engine itself.

Many of these components are developed in house at AdaCore, and many other components are developed primarily outside AdaCore (such as GCC, GDB, Why3, CVC4, ...). Such complex integration is only possible because all these components are Open Source and precisely allow this kind of combination. Add on top of that AdaCore's expertise in such integration and productization, and you get our ever growing offering!

Posted in #CodePeer    #QGen    #SPARK Pro    #Open Source   

About Arnaud Charlet

Arnaud Charlet is the lead of Product Engineering at AdaCore and the CodePeer product manager. In addition, he has recently led the design and implementation effort on the GNAT CCG technology and is the GNAT LLVM project manager. Arnaud previously worked on the implementation of the GNAT tasking runtime and on GNAT Programming Studio, both as a software engineer and as product manager.