CPROVER Manual TOC

Build Systems and Libraries

Variants of goto-cc

The goto-cc utility comes in several variants, summarised in the following table.

ExecutableEnvironmentPreprocessor
goto-cc gcc (control-flow graph only) gcc -E
goto-gcc gcc ("hybrid" executable) gcc -E
goto-armcc ARM RVDS armcc -E
goto-cl Visual Studio cl /E
goto-cw Freescale CodeWarrior mwcceppc

The primary difference between the variants is the preprocessor called. Furthermore, the language recognized varies slightly. The variants can be obtained by simply renaming the goto-cc executable. On Linux/MacOS, the variants can be obtained by creating a symbolic link.

The "hybrid" executables contain both the control-flow graph for verification purposes and the usual, executable machine code.