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

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

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

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

goto-cc-5.59.0                                      June 2022                                         GOTO-CC(1)

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.

       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.

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

goto-cc understands the options of gcc(1) plus the following.

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

       --functionname
              Set entry point to name.

       --native-compilercmd
              Invoke cmd as preprocessor or compiler.

       --native-linkercmd
              Invoke cmd as linker.

       --native-assemblercmd
              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.cstatic 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-suffixsuffix
              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-sourcefile
              Copy failing (preprocessed) source to file.

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

goto-cc[options]goto-gcc[options]goto-ld[options]goto-as[options]goto-bcc[options]goto-armcc[options]goto-cw[options]