FreeBSD Manual Pages
GOTO-CC(1) User Commands GOTO-CC(1) 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). 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 be- havior 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 bi- nary. 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 origi- nal 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 man- gling 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 trans- lation unit. We recommend using crangler(1) as a more configurable alternative. --mangle-suffix suffix Append suffix to exported file-local symbols. Use this option to- gether 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 ver- sions 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. BUGS If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues SEE ALSO as(1), bcc(1), cbmc(1), crangler(1), elf(5), gcc(1), ld(1) COPYRIGHT 2006-2018, Daniel Kroening, Michael Tautschnig, Christoph Wintersteiger goto-cc-5.59.0 June 2022 GOTO-CC(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | BACKWARD COMPATIBILITY | ENVIRONMENT | BUGS | SEE ALSO | COPYRIGHT
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=goto-gcc&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>