cprover
|
#include <gcc_mode.h>
Public Member Functions | |
int | doit () final |
does it. More... | |
void | help_mode () final |
display command line help More... | |
gcc_modet (goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary) | |
![]() | |
virtual int | main (int argc, const char **argv) |
starts the compiler More... | |
virtual void | help () |
display command line help More... | |
virtual void | usage_error () |
prints a message informing the user about incorrect options More... | |
goto_cc_modet (goto_cc_cmdlinet &, const std::string &_base_name, message_handlert &) | |
constructor More... | |
~goto_cc_modet () | |
constructor More... | |
Protected Member Functions | |
int | preprocess (const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc) |
call gcc for preprocessing More... | |
int | run_gcc (const compilet &compiler) |
call gcc with original command line More... | |
int | gcc_hybrid_binary (compilet &compiler) |
int | asm_output (bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler) |
![]() | |
void | register_languages () |
Static Protected Member Functions | |
static bool | needs_preprocessing (const std::string &) |
Protected Attributes | |
gcc_message_handlert | gcc_message_handler |
const bool | produce_hybrid_binary |
std::string | native_tool_name |
const std::string | goto_binary_tmp_suffix |
const std::map< std::string, std::set< std::string > > | arch_map |
Associate CBMC architectures with processor names. More... | |
gcc_versiont | gcc_version |
![]() | |
goto_cc_cmdlinet & | cmdline |
const std::string | base_name |
Additional Inherited Members |
Definition at line 25 of file gcc_mode.h.
gcc_modet::gcc_modet | ( | goto_cc_cmdlinet & | _cmdline, |
const std::string & | _base_name, | ||
bool | _produce_hybrid_binary | ||
) |
Definition at line 106 of file gcc_mode.cpp.
|
protected |
Definition at line 991 of file gcc_mode.cpp.
References goto_cc_modet::cmdline, comment(), messaget::debug(), messaget::eom(), messaget::error(), get_base_name(), cmdlinet::get_value(), cmdlinet::isset(), native_tool_name, goto_cc_cmdlinet::parsed_argv, produce_hybrid_binary, messaget::result(), and run_gcc().
Referenced by doit().
|
finalvirtual |
does it.
Implements goto_cc_modet.
Definition at line 320 of file gcc_mode.cpp.
References configt::ansi_c, configt::ansi_ct::arch, arch_map, asm_output(), compilet::ASSEMBLE_ONLY, goto_cc_modet::base_name, configt::ansi_ct::c_standard, CBMC_VERSION, configt::ansi_ct::char_is_unsigned, gcc_versiont::CLANG, configt::ansi_ct::CLANG, goto_cc_modet::cmdline, compilet::COMPILE_LINK, compilet::COMPILE_LINK_EXECUTABLE, compilet::COMPILE_ONLY, compiler_name(), config, configt::cpp, configt::cppt::cpp_standard, messaget::debug(), gcc_versiont::default_c_standard, gcc_versiont::default_cxx_standard, configt::ansi_ct::double_width, configt::ansi_ct::endianness, messaget::eom(), messaget::error(), messaget::eval_verbosity(), gcc_versiont::flavor, configt::ansi_ct::Float128_type, gcc_versiont::GCC, configt::ansi_ct::GCC, gcc_hybrid_binary(), gcc_message_handler, gcc_version, gcc_versiont::get(), get_base_name(), cmdlinet::get_value(), cmdlinet::get_values(), has_prefix(), has_suffix(), goto_cc_cmdlinet::have_infile_arg(), goto_cc_modet::help(), gcc_versiont::is_at_least(), configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, cmdlinet::isset(), compilet::LINK_LIBRARY, messaget::M_ERROR, messaget::M_WARNING, configt::ansi_ct::mode, native_tool_name, needs_preprocessing(), goto_cc_cmdlinet::parsed_argv, preprocess(), compilet::PREPROCESS_ONLY, configt::ansi_ct::preprocessor_options, produce_hybrid_binary, run_gcc(), configt::set(), configt::set_arch(), configt::ansi_ct::set_arch_spec_arm(), configt::ansi_ct::set_arch_spec_i386(), configt::ansi_ct::set_arch_spec_x86_64(), configt::ansi_ct::set_c11(), configt::ansi_ct::set_c89(), configt::ansi_ct::set_c99(), configt::cppt::set_cpp11(), configt::cppt::set_cpp14(), configt::ansi_ct::short_int_width, configt::ansi_ct::single_precision_constant, configt::ansi_ct::single_width, configt::this_architecture(), configt::this_operating_system(), configt::ansi_ct::ts_18661_3_Floatn_types, configt::ansi_ct::undefines, configt::ansi_ct::VISUAL_STUDIO, configt::ansi_ct::wchar_t_is_unsigned, and configt::ansi_ct::wchar_t_width.
|
protected |
Definition at line 884 of file gcc_mode.cpp.
References goto_cc_modet::base_name, goto_cc_modet::cmdline, compiler_name(), messaget::debug(), messaget::eom(), messaget::error(), gcc_message_handler, get_base_name(), messaget::get_message_handler(), cmdlinet::get_value(), goto_binary_tmp_suffix, has_suffix(), hybrid_binary(), cmdlinet::isset(), linker_name(), native_tool_name, needs_preprocessing(), goto_cc_cmdlinet::parsed_argv, messaget::result(), and run_gcc().
Referenced by doit().
|
finalvirtual |
|
staticprotected |
Definition at line 305 of file gcc_mode.cpp.
References has_suffix().
Referenced by doit(), and gcc_hybrid_binary().
|
protected |
call gcc for preprocessing
Definition at line 763 of file gcc_mode.cpp.
References goto_cc_modet::cmdline, messaget::debug(), messaget::eom(), has_prefix(), INVARIANT, native_tool_name, goto_cc_cmdlinet::parsed_argv, run(), and goto_cc_cmdlinet::stdin_file.
Referenced by doit().
|
protected |
call gcc with original command line
Definition at line 841 of file gcc_mode.cpp.
References goto_cc_modet::cmdline, compilet::cprover_macro_arities(), messaget::debug(), messaget::eom(), id2string(), native_tool_name, goto_cc_cmdlinet::parsed_argv, PRECONDITION, run(), goto_cc_cmdlinet::stdin_file, and compilet::wrote_object_files().
Referenced by asm_output(), doit(), and gcc_hybrid_binary().
|
protected |
Associate CBMC architectures with processor names.
Definition at line 46 of file gcc_mode.h.
Referenced by doit().
|
protected |
Definition at line 37 of file gcc_mode.h.
Referenced by doit(), and gcc_hybrid_binary().
|
protected |
Definition at line 66 of file gcc_mode.h.
Referenced by doit().
|
protected |
Definition at line 43 of file gcc_mode.h.
Referenced by gcc_hybrid_binary().
|
protected |
Definition at line 41 of file gcc_mode.h.
Referenced by asm_output(), doit(), gcc_hybrid_binary(), preprocess(), and run_gcc().
|
protected |
Definition at line 39 of file gcc_mode.h.
Referenced by asm_output(), and doit().