GOTO-CC(1) User Commands GOTO-CC(1)

# [NAME](#NAME)

goto-cc - C/C++ to goto compiler

# [SYNOPSIS](#SYNOPSIS)

**goto-cc \[options]**

**goto-gcc \[options]**

**goto-ld \[options]**

**goto-as \[options]**

**goto-bcc \[options]**

**goto-armcc \[options]**

**goto-cw \[options]**

# [DESCRIPTION](#DESCRIPTION)

**goto-cc** reads source code, and generates a GOTO binary. Its command-line interface is designed to mimic that of [**gcc**(1)](/man/os/cbmc/gcc.1). Note in particular that **goto-cc** distinguishes between compiling and linking phases, just as [**gcc**(1)](/man/os/cbmc/gcc.1) does. [**cbmc**(1)](/man/os/cbmc/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)](/man/os/cbmc/gcc.1) as preprocessor and builds an [**elf**(5)](/man/os/cbmc/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)](/man/os/cbmc/elf.5) object as above.

**goto-as**: invokes the system assembler [**as**(1)](/man/os/cbmc/as.1) and includes the original assembly source as a string in the output file.

**goto-bcc**: invokes [**bcc**(1)](/man/os/cbmc/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](#OPTIONS)

**goto-cc** understands the options of [**gcc**(1)](/man/os/cbmc/gcc.1) plus the following.

[**--verbosity** *N*](#verbosity)

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*](#function)

Set entry point to *name*.

[**--native-compiler** *cmd*](#native)

Invoke *cmd* as preprocessor or compiler.

[**--native-linker** *cmd*](#native~2)

Invoke *cmd* as linker.

[**--native-assembler** *cmd*](#native~3)

Invoke *cmd* as assembler (**goto-as** only).

[**--export-file-local-symbols**](#export)

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)](/man/os/cbmc/crangler.1) as a more configurable alternative.

[**--mangle-suffix suffix**](#mangle)

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*](#print)

Copy failing (preprocessed) source to *file*.

# [BACKWARD COMPATIBILITY](#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)](/man/os/cbmc/cbmc.1).

# [ENVIRONMENT](#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)](/man/os/cbmc/gcc.1) does.

# [BUGS](#BUGS)

If you encounter a problem please create an issue at **https://github.com/diffblue/cbmc/issues**

# [SEE ALSO](#SEE_ALSO)

[**as**(1)](/man/os/cbmc/as.1), [**bcc**(1)](/man/os/cbmc/bcc.1), [**cbmc**(1)](/man/os/cbmc/cbmc.1), [**crangler**(1)](/man/os/cbmc/crangler.1), [**elf**(5)](/man/os/cbmc/elf.5), [**gcc**(1)](/man/os/cbmc/gcc.1), [**ld**(1)](/man/os/cbmc/ld.1)

# [COPYRIGHT](#COPYRIGHT)

2006-2018, Daniel Kroening, Michael Tautschnig, Christoph Wintersteiger

June 2022 goto-cc-5.59.0

---

Document: goto-ld(1) from cbmc 6.11.0-r0 (Chainguard OS)