cprover
|
Globally accessible architectural configuration. More...
#include <config.h>
Classes | |
struct | ansi_ct |
struct | bv_encodingt |
struct | cppt |
struct | javat |
struct | verilogt |
Public Member Functions | |
void | set_arch (const irep_idt &) |
void | set_from_symbol_table (const symbol_tablet &) |
bool | set (const cmdlinet &cmdline) |
void | set_object_bits_from_symbol_table (const symbol_tablet &) |
Sets the number of bits used for object addresses. More... | |
std::string | object_bits_info () |
Static Public Member Functions | |
static irep_idt | this_architecture () |
static irep_idt | this_operating_system () |
Public Attributes | |
struct configt::ansi_ct | ansi_c |
struct configt::cppt | cpp |
struct configt::verilogt | verilog |
struct configt::javat | java |
struct configt::bv_encodingt | bv_encoding |
std::string | main |
Private Member Functions | |
void | set_classpath (const std::string &cp) |
std::string configt::object_bits_info | ( | ) |
Definition at line 1203 of file config.cpp.
References ansi_c, bv_encoding, configt::bv_encodingt::is_object_bits_default, configt::bv_encodingt::object_bits, configt::ansi_ct::pointer_width, and to_string().
Referenced by cbmc_parse_optionst::get_goto_program(), and jbmc_parse_optionst::get_goto_program().
bool configt::set | ( | const cmdlinet & | cmdline | ) |
Definition at line 738 of file config.cpp.
References ansi_c, configt::ansi_ct::arch, configt::ansi_ct::bool_width, bv_encoding, configt::ansi_ct::c_standard, configt::ansi_ct::char_is_unsigned, configt::ansi_ct::char_width, configt::ansi_ct::CLANG, cpp, configt::cppt::cpp_standard, configt::ansi_ct::default_c_standard(), configt::cppt::default_cpp_standard(), configt::bv_encodingt::default_object_bits, configt::ansi_ct::defines, configt::ansi_ct::double_width, configt::ansi_ct::endianness, configt::ansi_ct::Float128_type, configt::ansi_ct::for_has_scope, configt::ansi_ct::GCC, cmdlinet::get_value(), cmdlinet::get_values(), configt::ansi_ct::include_files, configt::ansi_ct::include_paths, configt::ansi_ct::int_width, configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, configt::bv_encodingt::is_object_bits_default, cmdlinet::isset(), java, configt::ansi_ct::lib, configt::ansi_ct::LIB_FULL, configt::ansi_ct::LIB_NONE, configt::ansi_ct::long_double_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, main, configt::javat::main_class, configt::ansi_ct::mode, configt::ansi_ct::NO_ENDIANNESS, configt::ansi_ct::NO_OS, configt::ansi_ct::NULL_is_zero, configt::bv_encodingt::object_bits, configt::ansi_ct::os, configt::ansi_ct::OS_LINUX, configt::ansi_ct::OS_MACOS, configt::ansi_ct::OS_WIN, configt::ansi_ct::pointer_width, configt::ansi_ct::preprocessor, ieee_floatt::ROUND_TO_EVEN, ieee_floatt::ROUND_TO_MINUS_INF, ieee_floatt::ROUND_TO_PLUS_INF, ieee_floatt::ROUND_TO_ZERO, configt::ansi_ct::rounding_mode, configt::ansi_ct::set_16(), configt::ansi_ct::set_32(), configt::ansi_ct::set_64(), set_arch(), set_classpath(), configt::ansi_ct::set_ILP32(), configt::ansi_ct::set_ILP64(), configt::ansi_ct::set_LLP64(), configt::ansi_ct::set_LP32(), configt::ansi_ct::set_LP64(), configt::ansi_ct::short_int_width, configt::ansi_ct::single_precision_constant, configt::ansi_ct::single_width, configt::ansi_ct::string_abstraction, this_architecture(), this_operating_system(), to_string(), configt::ansi_ct::ts_18661_3_Floatn_types, unsafe_string2unsigned(), configt::ansi_ct::VISUAL_STUDIO, configt::ansi_ct::wchar_t_is_unsigned, and configt::ansi_ct::wchar_t_width.
Referenced by as_modet::doit(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), ms_link_modet::doit(), ld_modet::doit(), gcc_modet::doit(), clobber_parse_optionst::get_command_line_options(), jdiff_parse_optionst::get_command_line_options(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), jbmc_parse_optionst::get_command_line_options(), janalyzer_parse_optionst::get_command_line_options(), goto_analyzer_parse_optionst::get_command_line_options(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), and goto_instrument_parse_optionst::get_goto_program().
void configt::set_arch | ( | const irep_idt & | arch | ) |
Definition at line 674 of file config.cpp.
References ansi_c, configt::ansi_ct::arch, configt::ansi_ct::endianness, configt::ansi_ct::lib, configt::ansi_ct::LIB_NONE, configt::ansi_ct::NO_ENDIANNESS, configt::ansi_ct::NULL_is_zero, configt::ansi_ct::set_32(), configt::ansi_ct::set_64(), configt::ansi_ct::set_arch_spec_alpha(), configt::ansi_ct::set_arch_spec_arm(), configt::ansi_ct::set_arch_spec_hppa(), configt::ansi_ct::set_arch_spec_i386(), configt::ansi_ct::set_arch_spec_ia64(), configt::ansi_ct::set_arch_spec_mips(), configt::ansi_ct::set_arch_spec_power(), configt::ansi_ct::set_arch_spec_s390(), configt::ansi_ct::set_arch_spec_s390x(), configt::ansi_ct::set_arch_spec_sh4(), configt::ansi_ct::set_arch_spec_sparc(), configt::ansi_ct::set_arch_spec_v850(), configt::ansi_ct::set_arch_spec_x32(), and configt::ansi_ct::set_arch_spec_x86_64().
Referenced by gcc_modet::doit(), set(), and set_from_symbol_table().
|
private |
Definition at line 1294 of file config.cpp.
References configt::javat::classpath, java, and split_string().
Referenced by set().
void configt::set_from_symbol_table | ( | const symbol_tablet & | symbol_table | ) |
Definition at line 1117 of file config.cpp.
References configt::ansi_ct::alignment, ansi_c, configt::ansi_ct::bool_width, configt::ansi_ct::char_is_unsigned, configt::ansi_ct::char_width, CPROVER_PREFIX, configt::ansi_ct::defines, configt::ansi_ct::double_width, configt::ansi_ct::endianness, id2string(), configt::ansi_ct::int_width, configt::ansi_ct::long_double_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, configt::ansi_ct::memory_operand_size, configt::ansi_ct::NULL_is_zero, configt::ansi_ct::os, configt::ansi_ct::pointer_width, set_arch(), set_object_bits_from_symbol_table(), configt::ansi_ct::short_int_width, configt::ansi_ct::single_width, string_from_ns(), configt::ansi_ct::string_to_os(), symbol_table_baset::symbols, this_architecture(), this_operating_system(), unsigned_from_ns(), configt::ansi_ct::wchar_t_is_unsigned, and configt::ansi_ct::wchar_t_width.
Referenced by read_object_and_link().
void configt::set_object_bits_from_symbol_table | ( | const symbol_tablet & | symbol_table | ) |
Sets the number of bits used for object addresses.
symbol_table | The symbol table |
Definition at line 1178 of file config.cpp.
References ansi_c, bv_encoding, cpp, CPROVER_PREFIX, DATA_INVARIANT, configt::ansi_ct::default_object_bits, configt::cppt::default_object_bits, configt::javat::default_object_bits, configt::bv_encodingt::is_object_bits_default, java, symbol_table_baset::lookup(), symbolt::mode, configt::bv_encodingt::object_bits, and configt::ansi_ct::pointer_width.
Referenced by language_uit::final(), lazy_goto_modelt::initialize(), initialize_goto_model(), and set_from_symbol_table().
|
static |
Definition at line 1213 of file config.cpp.
Referenced by as_modet::doit(), gcc_modet::doit(), jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), clobber_parse_optionst::help(), cbmc_parse_optionst::help(), goto_analyzer_parse_optionst::help(), set(), and set_from_symbol_table().
|
static |
Definition at line 1310 of file config.cpp.
Referenced by as_modet::doit(), gcc_modet::doit(), jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), clobber_parse_optionst::help(), cbmc_parse_optionst::help(), goto_analyzer_parse_optionst::help(), set(), and set_from_symbol_table().
struct configt::ansi_ct configt::ansi_c |
Referenced by compilet::add_compiler_specific_defines(), add_padding(), add_padding_gcc(), add_padding_msvc(), ansi_c_architecture_strings(), ansi_c_internal_additions(), value_set_dereferencet::build_reference_to(), builtin_factory(), byte_extract_id(), byte_update_id(), c_bool_type(), c_preprocess(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_none(), c_preprocess_visual_studio(), char_type(), goto_program2codet::cleanup_expr(), convert(), expr2ct::convert_code_decl(), dump_ct::convert_compound(), expr2ct::convert_constant(), convert_float_literal(), convert_integer_literal(), expr2ct::convert_rec(), boolbvt::convert_union(), expr2ct::convert_with_precedence(), boolbvt::convert_with_union(), cpp_convert_plain_type(), cpp_internal_additions(), cprover_c_library_factory(), cprover_cpp_library_factory(), c_typecheck_baset::do_special_functions(), as_modet::doit(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), gcc_modet::doit(), c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), generate_ansi_c_start_function(), c_typecastt::get_c_type(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), goto_analyzer_parse_optionst::get_command_line_options(), get_cprover_library_text(), goto_instrument_parse_optionst::instrument_goto_program(), string_abstractiont::is_char_type(), is_dereference_integer_object(), string_instrumentationt::is_string_type(), long_double_type(), value_set_dereferencet::memory_model_bytes(), c_typecastt::minimum_promotion(), model_argc_argv(), object_bits_info(), ansi_c_languaget::parse(), cpp_languaget::parse(), pointer_diff_type(), pointer_type(), print_struct_alignment_problems(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), reference_type(), set(), set_arch(), configt::ansi_ct::set_arch_spec_mips(), set_from_symbol_table(), set_object_bits_from_symbol_table(), signed_char_type(), signed_int_type(), signed_long_int_type(), signed_long_long_int_type(), signed_poly_type(), signed_short_int_type(), simplify_exprt::simplify_inequality_constant(), simplify_json_expr(), simplify_exprt::simplify_typecast(), size_type(), cpp_typecheckt::standard_conversion_floating_point_promotion(), cpp_typecheckt::standard_conversion_integral_promotion(), ansi_c_languaget::to_expr(), ansi_c_declarationt::to_symbol(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_type(), unsigned_char_type(), unsigned_int_type(), unsigned_long_int_type(), unsigned_long_long_int_type(), unsigned_poly_type(), unsigned_short_int_type(), wchar_t_type(), and xml().
struct configt::bv_encodingt configt::bv_encoding |
Referenced by bv_pointerst::bv_pointerst(), smt2_convt::convert_address_of_rec(), smt2_convt::convert_expr(), smt2_convt::convert_is_dynamic_object(), smt2_convt::define_object_size(), object_bits_info(), smt2_convt::parse_rec(), set(), set_object_bits_from_symbol_table(), and simplify_exprt::simplify_pointer_offset().
struct configt::cppt configt::cpp |
Referenced by c_preprocess_gcc_clang(), ms_cl_modet::doit(), gcc_modet::doit(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), goto_analyzer_parse_optionst::get_command_line_options(), cpp_parsert::parse(), set(), and set_object_bits_from_symbol_table().
struct configt::javat configt::java |
std::string configt::main |
Definition at line 171 of file config.h.
Referenced by ansi_c_entry_point(), get_main_symbol(), jsil_entry_point(), load_java_class(), model_argc_argv(), dump_ct::operator()(), parse_cover_options(), remove_internal_symbols(), and set().
struct configt::verilogt configt::verilog |