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.
- --verbosity
N
- 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.
- --function
name
- Set entry point to name.
- --native-compiler
cmd
- Invoke cmd as preprocessor or compiler.
- --native-linker
cmd
- Invoke cmd as linker.
- --native-assembler
cmd
- Invoke cmd as assembler (goto-as only).
- --export-file-local-symbols
- 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.
- --mangle-suffix
suffix
- 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.
- --print-rejected-preprocessed-source
file
- Copy failing (preprocessed) source to file.
- --object-bits
N
- Configure the number of bits used for object numbering in CBMC's pointer
encoding.
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