CBMC
bcc_cmdline.cpp File Reference

A special command line object for Bruce's C Compiler. More...

#include "bcc_cmdline.h"
#include <util/invariant.h>
#include <util/prefix.h>
#include <iostream>
+ Include dependency graph for bcc_cmdline.cpp:

Go to the source code of this file.

Variables

const char * goto_bcc_options_with_argument []
 
const char * bcc_options_without_argument []
 
const char * bcc_options_with_argument []
 

Detailed Description

A special command line object for Bruce's C Compiler.

Definition in file bcc_cmdline.cpp.

Variable Documentation

◆ bcc_options_with_argument

const char* bcc_options_with_argument[]
Initial value:
=
{
"-A",
"-B",
"-D",
"-U",
"-M",
"-o",
"-C",
"-P",
"-I",
"-L",
"-T",
"-Q",
"-t",
nullptr
}

Definition at line 52 of file bcc_cmdline.cpp.

◆ bcc_options_without_argument

const char* bcc_options_without_argument[]
Initial value:
=
{
"-0",
"-3",
"-E",
"-G",
"-N",
"-O",
"-P",
"-S",
"-V",
"-c",
"-e",
"-g",
"-v",
"-w",
"-x",
"-W",
"-ansi",
nullptr
}

Definition at line 30 of file bcc_cmdline.cpp.

◆ goto_bcc_options_with_argument

const char* goto_bcc_options_with_argument[]
Initial value:
=
{
"--verbosity",
"--function",
"--native-compiler",
"--native-linker",
"--print-rejected-preprocessed-source",
nullptr
}

Definition at line 20 of file bcc_cmdline.cpp.