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

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