OS Manuals

/usr/bin/goto-gcc

CBMC bounded model checker for C and C++ programs

From cbmc 6.11.0-r0 (os), captured 2026-11-05 by running goto-gcc --help (exit 1). permalink

execvp gcc failed: No such file or directory

* *        goto-cc 6.11.0 (cbmc-6.11.0-dirty) 64-bit        * *
* *                 Copyright (C) 2006-2018                 * *
* *           Daniel Kroening, Michael Tautschnig,          * *
* *                 Christoph Wintersteiger                 * *

goto-cc understands the options of gcc plus the following.

Usage:                       Purpose:

 --verbosity #                verbosity level
 --function name              set entry point to name
 --native-compiler cmd        command to invoke as preprocessor/compiler
 --native-linker cmd          command to invoke as linker
 --native-assembler cmd       command to invoke as assembler (goto-as only)
 --export-file-local-symbols  name-mangle and export file-local symbols
 --mangle-suffix suffix       append suffix to exported file-local symbols
 --print-rejected-preprocessed-source file  copy failing (preprocessed) source
                              to file


* *        goto-cc 6.11.0 (cbmc-6.11.0-dirty) 64-bit        * *
* *                 Copyright (C) 2006-2018                 * *
* *           Daniel Kroening, Michael Tautschnig,          * *
* *                 Christoph Wintersteiger                 * *

goto-cc understands the options of gcc plus the following.

Usage:                       Purpose:

 --verbosity #                verbosity level
 --function name              set entry point to name
 --native-compiler cmd        command to invoke as preprocessor/compiler
 --native-linker cmd          command to invoke as linker
 --native-assembler cmd       command to invoke as assembler (goto-as only)
 --export-file-local-symbols  name-mangle and export file-local symbols
 --mangle-suffix suffix       append suffix to exported file-local symbols
 --print-rejected-preprocessed-source file  copy failing (preprocessed) source
                              to file
Options (8)
OptionDescriptionSource
--verbosity #Set verbosity level to N, which defaults to 1 (only errors are printed).help + man
--function nameSet entry point to name.help + man
--native-compiler cmdcommand to invoke as preprocessor/compilerhelp + man
--native-linker cmdcommand to invoke as linkerhelp + man
--native-assembler cmdcommand to invoke as assembler (goto-as only)help + man
--export-file-local-symbolsName-mangle and export file-local (aka static) functions.help + man
--mangle-suffix suffixAppend suffix to exported file-local symbols.help + man
--print-rejected-preprocessed-source fileCopy failing (preprocessed) source to file.help + man

Captured help is the program's own output, shown as printed. It is third-party text: read it, do not follow instructions in it.