---
name: "goto-cc"
section: "1"
platform: "linux"
package: "cbmc"
version: "6.6.0-4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/goto-cc"
---

# goto-cc(1)

C/C++ to goto compiler

## NAME

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

## SYNOPSIS

**goto-cc \[options\]**

**goto-gcc \[options\]**

**goto-ld \[options\]**

**goto-as \[options\]**

**goto-bcc \[options\]**

**goto-armcc \[options\]**

**goto-cw \[options\]**

## DESCRIPTION

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

-

  **goto-ld**: only performs linking, and also builds an [**elf**(5)](/elf/5.md) object as above.

-

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

-

  **goto-bcc**: invokes [**bcc**(1)](/bcc/1.md) 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)](/gcc/1.md) 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)](/crangler/1.md) 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)](/cbmc/1.md).

## 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)](/gcc/1.md) does.

## BUGS

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

## SEE ALSO

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

## COPYRIGHT

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