Man page - goto-ld(1)

Packages contains this manual

Manual

GOTO-CC

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
BACKWARD COMPATIBILITY
ENVIRONMENT
BUGS
SEE ALSO
COPYRIGHT

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