goto-gcc(1) · carta

Usage

goto-cc [options]

goto-gcc [options]

goto-ld [options]

goto-as [options]

goto-bcc [options]

goto-armcc [options]

goto-cw [options]

Overview

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.

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.

Backward compatibility

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).

Environment

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.

History

Debian 13 (Trixie): the text shown here
Debian 11 (Bullseye)
Debian 10 (Buster) to Debian 9 (Stretch)

--export-file-local-symbols since Debian 13 (Trixie); --mangle-suffix since Debian 13 (Trixie); --native-assembler since Debian 13 (Trixie); --native-compiler since Debian 13 (Trixie); --native-linker since Debian 13 (Trixie); --print-rejected-preprocessed-source since Debian 13 (Trixie); --verbosity since Debian 13 (Trixie).

--16 until Debian 11 (Bullseye); --32 until Debian 11 (Bullseye); --64 until Debian 11 (Bullseye); --ILP32 until Debian 11 (Bullseye); --ILP64 until Debian 11 (Bullseye); --LLP64 until Debian 11 (Bullseye); --LP32 until Debian 11 (Bullseye); --LP64 until Debian 11 (Bullseye); --all-properties until Debian 11 (Bullseye); --arch until Debian 11 (Bullseye); --arrays-uf-always until Debian 11 (Bullseye); --arrays-uf-never until Debian 11 (Bullseye); --beautify-greedy until Debian 11 (Bullseye); --big-endian until Debian 11 (Bullseye); --boolector until Debian 11 (Bullseye); --bounds-check until Debian 11 (Bullseye); --cover-assertions until Debian 11 (Bullseye); --cvc until Debian 10 (Buster); --cvc3 until Debian 11 (Bullseye); --cvc4 until Debian 11 (Bullseye); --depth until Debian 11 (Bullseye); --dimacs until Debian 11 (Bullseye); --div-by-zero-check until Debian 11 (Bullseye); --dump-c until Debian 11 (Bullseye); --error-label until Debian 11 (Bullseye); --isr until Debian 11 (Bullseye); --little-endian until Debian 11 (Bullseye); --mathsat until Debian 11 (Bullseye); --mmio until Debian 11 (Bullseye); --nan-check until Debian 11 (Bullseye); --no-arch until Debian 11 (Bullseye); --no-assertions until Debian 11 (Bullseye); --no-assumptions until Debian 11 (Bullseye); --no-library until Debian 11 (Bullseye); --no-pretty-names until Debian 11 (Bullseye); --no-unwinding-assertions until Debian 11 (Bullseye); --nondet-static until Debian 11 (Bullseye); --nondet-volatile until Debian 11 (Bullseye); --os until Debian 11 (Bullseye); --outfile until Debian 11 (Bullseye); --pointer-check until Debian 11 (Bullseye); --preprocess until Debian 11 (Bullseye); --program-only until Debian 11 (Bullseye); --property until Debian 11 (Bullseye); --refine until Debian 11 (Bullseye); --round-to-minus-inf until Debian 11 (Bullseye); --round-to-nearest until Debian 11 (Bullseye); --round-to-plus-inf until Debian 11 (Bullseye); --round-to-zero until Debian 11 (Bullseye); --show-goto-functions until Debian 11 (Bullseye); --show-loops until Debian 11 (Bullseye); --show-properties until Debian 11 (Bullseye); --show-symbol-table until Debian 11 (Bullseye); --show-vcc until Debian 11 (Bullseye); --signed-overflow-check until Debian 11 (Bullseye); --slice-formula until Debian 11 (Bullseye); --smt2 until Debian 11 (Bullseye); --unsigned-char until Debian 11 (Bullseye); --unsigned-overflow-check until Debian 11 (Bullseye); --unwind until Debian 11 (Bullseye); --unwindset until Debian 11 (Bullseye); --yices until Debian 11 (Bullseye); --z3 until Debian 11 (Bullseye); -D until Debian 11 (Bullseye); -I until Debian 11 (Bullseye).