goto-cc – a C/C++ front-end for Verification

About goto-cc

goto-cc is a compiler that compiles programs given in a C and C++ into GOTO-programs (i.e., control-flow graphs). goto-cc can be run in the following environments:

As a replacement for gcc, which means that you can replace gcc in your makefiles or configure scripts with goto-cc and obtain a GOTO-binary instead of a real binary. goto-cc supports the usual extensions to the ANSI-C language that gcc offers.
As a replacement for Microsoft's Visual Studio compiler. In this mode, goto-cc supports Microsoft's extensions to the ANSI-C language.

The resulting goto-binaries are not meant to be executable, but are typically given to a verification or testing tool like SATABS or CBMC. As an additional feature, goto-cc generates dot-style flowgraphs of your functions!

You should also read the license.

goto-cc News

NEW: There is now a Google Group for annoucements related to the CPROVER tools.

NEW: goto-cc now processes most parts of the Linux Kernel without any need for modifications. The CPROVER manual contains instructions.

Documentation

There is a section on goto-cc in the CPROVER manual.

Download

You can get goto-cc (in binary and source form) by downloading and installing CBMC.

Funding

This research is currently supported by EPSRC grant EP/H017585/1.