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!