.TH GOTO-CC "1" "June 2022" "goto-cc-5.59.0" "User Commands"
.SH NAME
goto\-cc \- C/C++ to goto compiler
.SH SYNOPSIS
.B goto-cc [options]

.B goto-gcc [options]

.B goto-ld [options]

.B goto-as [options]

.B goto-bcc [options]

.B goto-armcc [options]

.B goto-cw [options]

.SH DESCRIPTION
.B goto\-cc
reads source code, and generates a GOTO binary. Its
command-line interface is designed to mimic that of
.BR gcc (1).
Note in particular that \fBgoto-cc\fR distinguishes between compiling
and linking phases, just as \fBgcc\fR(1) does. \fBcbmc\fR(1) expects a GOTO binary
for which linking has been completed.
.PP
The basename of the file that is used to invoke \fBgoto-cc\fR controls which
behavior will be emulated. This is typically accomplished by using symbolic
links.
.IP
\fBgoto-cc\fR: invokes the default system compiler as preprocessor and just
builds a GOTO binary.
.IP
\fBgoto-gcc\fR: invokes \fBgcc\fR(1) as preprocessor and builds an \fBelf\fR(5)
object file including an additional \fIgoto-cc\fR section that holds the GOTO
binary.
.IP
\fBgoto-ld\fR: only performs linking, and also builds an \fBelf\fR(5) object as
above.
.IP
\fBgoto-as\fR: invokes the system assembler \fBas\fR(1) and includes the
original assembly source as a string in the output file.
.IP
\fBgoto-bcc\fR: invokes \fBbcc\fR(1) as preprocessor.
.IP
\fBgoto-armcc\fR: invokes \fBarmcc\fR as preprocessor and enables support for
the ARM's C dialect and command-line options.
.IP
\fBgoto-cw\fR: invokes \fBmwcceppc\fR as preprocessor and enables support for
CodeWarrior's C dialect and command-line options.
.SH OPTIONS
.B goto\-cc
understands the options of \fBgcc\fR(1) plus the following.
.TP
\fB\-\-verbosity\fR \fIN\fR
Set verbosity level to \fIN\fR, which defaults to 1 (only errors are printed). A
verbosity of 0 disables all output. Using a verbosity of 2 or greater, or using
\fB\-Wall\fR enables warnings. Verbosity levels 4, 6, 8, 9, or 10 add increasing
amounts of debug information.
.TP
\fB\-\-function\fR \fIname\fR
Set entry point to \fIname\fR.
.TP
\fB\-\-native\-compiler\fR \fIcmd\fR
Invoke \fIcmd\fR as preprocessor or compiler.
.TP
\fB\-\-native\-linker\fR \fIcmd\fR
Invoke \fIcmd\fR as linker.
.TP
\fB\-\-native\-assembler\fR \fIcmd\fR
Invoke \fIcmd\fR as assembler (\fBgoto\-as\fR only).
.TP
\fB\-\-export\-file\-local\-symbols\fR
Name-mangle and export file-local (aka \fBstatic\fR) functions. Name mangling
prefixes each symbol name by \fB__CPROVER_file_local\fR and the basename of the
file. For example,

.EX
.in +4n
\fB// foo.c\fP
\fBstatic\fP int \fBbar\fP();
.in
.EE

yields a globally visible \fI__CPROVER_file_local_foo_c_bar\fR function.
Note that this approach mangles all functions contained in a translation unit.
We recommend using \fBcrangler\fR(1) as a more configurable alternative.
.TP
\fB\-\-mangle\-suffix \fIsuffix\fR
Append \fIsuffix\fR to exported file-local symbols. Use this option together
with \fB\-\-export\-file\-local\-symbols\fR when multiple files of the same base
name contain a \fBstatic\fR function of the same name. If so, use a unique
suffix in at least one of the \fBgoto\-cc\fR invocations used in compiling those
files.
.TP
\fB\-\-print\-rejected\-preprocessed\-source\fR \fIfile\fR
Copy failing (preprocessed) source to \fIfile\fR.
.SH BACKWARD COMPATIBILITY
.B goto\-cc
will warn and ignore the use of \fB\-\-object\-bits\fR, which previous versions
processed. This option now instead needs to be passed to \fBcbmc\fR(1).
.SH ENVIRONMENT
All tools honor the TMPDIR environment variable when generating temporary
files and directories.
.B goto\-cc
aims to accept all environment variables that \fBgcc\fR(1) does.
.SH BUGS
If you encounter a problem please create an issue at
.B https://github.com/diffblue/cbmc/issues
.SH SEE ALSO
.BR as (1),
.BR bcc (1),
.BR cbmc (1),
.BR crangler (1),
.BR elf (5),
.BR gcc (1),
.BR ld (1)
.SH COPYRIGHT
2006\-2018, Daniel Kroening, Michael Tautschnig, Christoph Wintersteiger