GOTO-CC(1)

💅 GOTO-CC ✨

okay bestie, welcome to the goto-cc manual page, from the User Commands section of the manual. she's a C/C++ to goto compiler and she's literally so iconic. let's get into it 🫶

---

🎀 NAME 🎀

goto-cc — C/C++ to goto compiler. that's it, that's the name, no notes 💖

---

🌸 SYNOPSIS 🌸

goto-cc [options]

goto-gcc [options]

goto-ld [options]

goto-as [options]

goto-bcc [options]

goto-armcc [options]

goto-cw [options]

seven whole personalities, one binary. the range?? unmatched 👑

---

✨ DESCRIPTION ✨

so goto-cc reads your source code and generates a GOTO binary. her command-line interface is designed to mimic gcc(1), so if you already know gcc you're basically already friends with her. and pay attention bestie: goto-cc distinguishes between the compiling and linking phases, just like gcc(1) does. cbmc(1) expects a GOTO binary where the linking has been completed — so don't show up half-done, she will notice 🙈

here's the fun part: the basename of the file you use to invoke goto-cc controls which behavior gets emulated. and how do you get different basenames? symbolic links, obviously. that's the whole trick ✨

• 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. yes, all of gcc's options. she's fluent 💅

• --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. that option now instead needs to be passed to cbmc(1). so if you're carrying that flag around like an old situationship, she's gonna warn you and move on 😭

---

🌈 ENVIRONMENT 🌈

all tools honor the TMPDIR environment variable when generating temporary files and directories. and goto-cc aims to accept all environment variables that gcc(1) does. she's accommodating like that 🫶

---

💀 BUGS 💀

if you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues. she wants to hear about it, fr fr. no gatekeeping 🙈

---

👑 SEE ALSO 👑

as(1), bcc(1), cbmc(1), crangler(1), elf(5), gcc(1), ld(1)

the whole friend group, all linked in the see-also section. iykyk 💜

---

💖 COPYRIGHT 💖

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

---

and that's the whole page bestie, you ate it, no crumbs 💅 this was goto-cc-5.59.0 from June 2022 — go compile something iconic, periodt 🎀✨🦋