goto-cc - C/C++ to goto compiler
goto-cc [options]
goto-gcc [options]
goto-ld [options]
goto-as [options]
goto-bcc [options]
goto-armcc [options]
goto-cw [options]
goto-cc reads source code, and generates a GOTO binary. Its command-line interface is designed to mimic that of gcc(1). Note in particular that goto-cc distinguishes between compiling and linking phases, just as gcc(1) does. cbmc(1) expects a GOTO binary for which linking has been completed.
The basename of the file that is used to invoke goto-cc controls which behavior will be emulated. This is typically accomplished by using symbolic links.
goto-cc: invokes the default system compiler as preprocessor and just builds a GOTO binary.
goto-gcc: invokes gcc(1) as preprocessor and builds an elf(5) object file including an additional goto-cc section that holds the GOTO binary.
goto-ld: only performs linking, and also builds an elf(5) object as above.
goto-as: invokes the system assembler as(1) and includes the original assembly source as a string in the output file.
goto-bcc: invokes bcc(1) as preprocessor.
goto-armcc: invokes armcc as preprocessor and enables support for the ARM's C dialect and command-line options.
goto-cw: invokes mwcceppc as preprocessor and enables support for CodeWarrior's C dialect and command-line options.
goto-cc understands the options of gcc(1) plus the following.
Set verbosity level to N, which defaults to 1 (only errors are printed). A verbosity of 0 disables all output. Using a verbosity of 2 or greater, or using -Wall enables warnings. Verbosity levels 4, 6, 8, 9, or 10 add increasing amounts of debug information.
Set entry point to name.
Invoke cmd as preprocessor or compiler.
Invoke cmd as linker.
Invoke cmd as assembler (goto-as only).
Name-mangle and export file-local (aka static) functions. Name mangling prefixes each symbol name by __CPROVER_file_local and the basename of the file. For example,
// foo.c
static int bar();yields a globally visible __CPROVER_file_local_foo_c_bar function. Note that this approach mangles all functions contained in a translation unit. We recommend using crangler(1) as a more configurable alternative.
Append suffix to exported file-local symbols. Use this option together with --export-file-local-symbols when multiple files of the same base name contain a static function of the same name. If so, use a unique suffix in at least one of the goto-cc invocations used in compiling those files.
Copy failing (preprocessed) source to file.
goto-cc will warn and ignore the use of --object-bits, which previous versions processed. This option now instead needs to be passed to cbmc(1).
All tools honor the TMPDIR environment variable when generating temporary files and directories. goto-cc aims to accept all environment variables that gcc(1) does.
If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues
as(1), bcc(1), cbmc(1), crangler(1), elf(5), gcc(1), ld(1)
2006-2018, Daniel Kroening, Michael Tautschnig, Christoph Wintersteiger