CPROVER Manual TOC
The goto-cc utility comes in several variants, summarised in the following table.
|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|
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.