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.

Documentation

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