The first and only formally verified C compiler for safety-critical TriCore applications

CompCert for TriCore is a formally verified optimizing C compiler. Its intended use is compiling safety-critical software and meeting the highest levels of assurance.

Can you trust your compiler?

Compilers are complicated pieces of software that implement delicate algorithms. Bugs in compilers do occur and can cause incorrect executable code to be silently generated from a correct source program. In other words, a buggy compiler can insert bugs in the programs that it compiles.

Time and again, studies have shown that many popular production compilers suffer from miscompilation issues.

• As early as in 1995, the authors of the Nullstone C conformance test suite reported

  [integer-division] defects in twelve of twenty commercially available compilers that were evaluated.

• A decade later, E. Eide and J. Regehr showed similar sloppiness in C compilers, this time concerning volatile memory accesses:

  We tested thirteen production-quality C compilers and, for each, found situations in which the compiler generated incorrect code for accessing volatile variables. This result is disturbing because it implies that embedded software and operating systems — both typically coded in C, both being bases for many mission-critical and safety-critical applications, and both relying on the correct translation of volatiles — may be being miscompiled.

• More recently, Regehr, Yang et al. generalized their testing of C compilers and, again, found many instances of miscompilation:

We created a tool that generates random C programs, and then spent two and a half years using it to find compiler bugs. So far, we have reported more than 325 previously unknown bugs to compiler developers. Moreover, every compiler that we tested has been found to crash and also to silently generate wrong code when presented with valid inputs.

What sets CompCert apart?

CompCert is the only production compiler that is formally verified, using machine-assisted math­ematical proofs, to be exempt from mis­compilation issues. The code it pro­duces is proved to behave exactly as specified by the semantics of the source C program.

Your benefits

• CompCert is a natural complement to any verification tech­niques that you apply at the source-code level — be it model checking, program proof, or static analyzers such as Astrée or RuleChecker. Only with CompCert can you guarantee that all the safety pro­perties verified on the source code also hold for the ge­nerated machine code.

• CompCert supports verified separate compilation, enabling large-scale verification of complex software created by many different teams each working on C modules of their own.

• When using a conventional compiler to compile safety-critical applications, you typically have to disable compiler optimizations and run into resource problems as a result. With CompCert, you can significantly improve your applications’ performance, as you no longer have to switch off optimizations for safety reasons.

Formally verified optimizations

CompCert implements the following optimizations, all of them formally verified:

• Register allocation using graph coloring and iterated register coalescing
• Instruction selection with strength reduction
• Constant propagation for integer and floating-point types
• Common subexpression elimination
• Dead code elimination
• Redundant code elimination
• Function inlining
• Tail call elimination
• If-conversion

Loop optimizations are currently not performed, but can be implemented on request.

Compilation with execution time in mind

On average, code generated by CompCert is:

• twice as fast as code generated by GCC without optimizations,
• only 10% slower than GCC code at optimization level 1,
• some 20% slower than GCC code at optimization level 3.

Due to the lack of aggressive loop optimizations, performance is lower for code that involves many matrix computations.

Ease-of-use and interoperability

• From command-line options to error messages to the handling of built-in functions, many CompCert features are very deliberately implemented to feel familiar and intuitive to GCC and LLVM users.
• Another express goal is to generate object code that respects the Application Binary Interface (ABI) of the target platform, and thus can be linked with object code and libraries compiled by other C compilers. In this, CompCert succeeds to a great extent, with some exceptions that are thoroughly documented.
• CompCert for TriCore is supported by the entire chain of AbsInt tools for safety-critical and mission-critical TriCore applications:
  • Astrée for sound static analysis of your C code
  • RuleChecker for proving compliance with MISRA, CERT, CWE, and other standards
  • ValueAnalyzer for uncovering illegal accesses from within third-party object code
  • StackAnalyzer for static analysis of the worst-case stack usage
  • aiT for safe and precise static WCET analysis
  • TimeWeaver for hybrid WCET analysis
  • TimingProfiler for WCET estimates at early stages of software development

© 2025 AbsInt. Published by JORAL Technologies.