Elevating AdaCore’s C compiler to Ada/SPARK safety

Leading one-stop-shop developer of Ada and SPARK tool sets uses SuperTest to validate its C compiler for mixed-language programming environments    

 

AdaCore, a world leader in tools and services for high-integrity software development, provides comprehensive support for the Ada and SPARK programming languages. Both languages have gained significant traction in safety-critical application areas such as railway, avionics and automotive systems, where reliability, safety and security are paramount. However, as Vasiliy Fofanov, Senior Software Engineer in AdaCore’s Paris office points out, most application development teams are rarely purist in their choice of language.

 

“In practice, many of our customers have systems that use several different languages at the same time. Most of the code may be written in Ada or SPARK but they also have some secondary algorithms implemented in C. Because they don’t want to have to deal with multiple software tool suppliers, many of them also ask us to provide solutions for C,” he says. “Our expertise in high-integrity software development tools also means that we are often approached by companies that do not use Ada – so not our traditional customers – to provide a C tool chain with the same safety guarantees that we provide for Ada and SPARK.”

 

Both types of customer demand mean that AdaCore needs to supply C compilers, and to ensure that they meet the safety requirements of its customers, it needs to verify them to international standards such as ISO 26262. That’s where SuperTest came to the rescue. AdaCore is using SuperTest to verify the front-end of a C compiler that is common to many of the target instruction set architectures it supports, including ARM 32- and 64-bit, PowerPC 32- and 64-bit, native Windows, Linux, and more recently, RISC-V.

 

According to Vasiliy, getting SuperTest up and running to suit AdaCore’s customized GCC compiler was relatively straightforward, although not completely hassle free.

 

“Our GCC compiler is a customized version, so it’s not always in sync with the standard GCC community releases. As a result, there were some tests in SuperTest that were not applicable, but they were quickly analysed and removed from the test suite,” he says. “There were also a few problems with the scripting, but the Solid Sands team were very responsive, and the issues quickly sorted out. We never expected it to be a walk in the park, but overall it was a very positive experience.”

 

AdaCore did not take its own compiler verification efforts for granted. In fact, the principal aim of using SuperTest was to gain external approval for its C compiler. It therefore subjected its methodology and verification results to independent external auditing, which it successfully passed.

 

“In terms of safety and security, I think our C compiler is now pretty much on the same level as our Ada and SPARK tool set, so we are now in a position to offer the same compiler quality to our safety-conscious C customers as we are for Ada and SPARK,” says Vasiliy.  “For new projects we would obviously recommend they go for SPARK, because even if the compiler faithfully translates a C program into object code this does not necessarily mean that the original C program is safe. With SPARK, program safety comes straight out of the box.”

 

Nevertheless, with C’s ubiquity and its huge ecosystem of available target processors, tools and devotees, he concedes that C will continue to be a significant part of the language mix.

 

“We appreciate that many customers, especially when they get closer and closer to the target architecture, prefer to write those ‘close-in’ segments of code in C. So having a mix of SPARK, Ada and C in the final solution will not be uncommon. The important thing is that thanks to SuperTest we can now provide the same level of tool assurance for all three languages.”