goto-cc – a C/C++ front-end for Verification
goto-cc is a compiler that compiles programs given in a
C and C++ into GOTO-programs (i.e., control-flow graphs).
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-ccsupports the usual extensions to the ANSI-C language that gcc offers.
As a replacement for Microsoft's Visual Studio compiler. In this mode,
goto-ccsupports 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,
of your functions!
You should also read the license.
NEW: There is now a Google Group for annoucements related to the CPROVER tools.
goto-cc now processes most parts of the Linux
Kernel without any need for modifications. The CPROVER
There is a
goto-cc in the CPROVER manual.
You can get
goto-cc (in binary and source form)
by downloading and installing CBMC.
This research is currently supported by EPSRC grant EP/H017585/1.