cprover
|
#include <config.h>
Public Member Functions | |
void | set_c89 () |
void | set_c99 () |
void | set_c11 () |
void | set_16 () |
void | set_32 () |
void | set_64 () |
void | set_LP64 () |
int=32, long=64, pointer=64 More... | |
void | set_ILP64 () |
int=64, long=64, pointer=64 More... | |
void | set_LLP64 () |
int=32, long=32, pointer=64 More... | |
void | set_ILP32 () |
int=32, long=32, pointer=32 More... | |
void | set_LP32 () |
int=16, long=32, pointer=32 More... | |
void | set_arch_spec_i386 () |
void | set_arch_spec_x86_64 () |
void | set_arch_spec_power (const irep_idt &subarch) |
void | set_arch_spec_arm (const irep_idt &subarch) |
void | set_arch_spec_alpha () |
void | set_arch_spec_mips (const irep_idt &subarch) |
void | set_arch_spec_s390 () |
void | set_arch_spec_s390x () |
void | set_arch_spec_sparc (const irep_idt &subarch) |
void | set_arch_spec_ia64 () |
void | set_arch_spec_x32 () |
void | set_arch_spec_v850 () |
Sets up the widths of variables for the Renesas V850. More... | |
void | set_arch_spec_hppa () |
void | set_arch_spec_sh4 () |
Static Public Member Functions | |
static c_standardt | default_c_standard () |
static std::string | os_to_string (ost) |
static ost | string_to_os (const std::string &) |
Public Attributes | |
std::size_t | int_width |
std::size_t | long_int_width |
std::size_t | bool_width |
std::size_t | char_width |
std::size_t | short_int_width |
std::size_t | long_long_int_width |
std::size_t | pointer_width |
std::size_t | single_width |
std::size_t | double_width |
std::size_t | long_double_width |
std::size_t | wchar_t_width |
bool | char_is_unsigned |
bool | wchar_t_is_unsigned |
bool | for_has_scope |
bool | ts_18661_3_Floatn_types |
bool | Float128_type |
bool | single_precision_constant |
enum configt::ansi_ct::c_standardt | c_standard |
ieee_floatt::rounding_modet | rounding_mode |
std::size_t | alignment |
std::size_t | memory_operand_size |
endiannesst | endianness |
ost | os |
irep_idt | arch |
bool | NULL_is_zero |
flavourt | mode |
preprocessort | preprocessor |
std::list< std::string > | defines |
std::list< std::string > | undefines |
std::list< std::string > | preprocessor_options |
std::list< std::string > | include_paths |
std::list< std::string > | include_files |
libt | lib |
bool | string_abstraction |
Static Public Attributes | |
static const std::size_t | default_object_bits =8 |
|
strong |
|
strong |
|
strong |
|
strong |
|
strong |
|
strong |
|
static |
Definition at line 647 of file config.cpp.
Referenced by cbmc_parse_optionst::help(), goto_analyzer_parse_optionst::help(), and configt::set().
|
static |
Definition at line 1041 of file config.cpp.
Referenced by ansi_c_architecture_strings().
void configt::ansi_ct::set_16 | ( | ) |
void configt::ansi_ct::set_32 | ( | ) |
Definition at line 30 of file config.cpp.
Referenced by configt::set(), and configt::set_arch().
void configt::ansi_ct::set_64 | ( | ) |
Definition at line 35 of file config.cpp.
Referenced by configt::set(), and configt::set_arch().
void configt::ansi_ct::set_arch_spec_alpha | ( | ) |
Definition at line 321 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_arm | ( | const irep_idt & | subarch | ) |
Definition at line 278 of file config.cpp.
References UNREACHABLE.
Referenced by gcc_modet::doit(), and configt::set_arch().
void configt::ansi_ct::set_arch_spec_hppa | ( | ) |
Definition at line 588 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_i386 | ( | ) |
Definition at line 148 of file config.cpp.
References UNREACHABLE.
Referenced by gcc_modet::doit(), and configt::set_arch().
void configt::ansi_ct::set_arch_spec_ia64 | ( | ) |
Definition at line 497 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_mips | ( | const irep_idt & | subarch | ) |
Definition at line 350 of file config.cpp.
References configt::ansi_c, config, pointer_width, to_string(), and UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_power | ( | const irep_idt & | subarch | ) |
Definition at line 217 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_s390 | ( | ) |
Definition at line 400 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_s390x | ( | ) |
Definition at line 429 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_sh4 | ( | ) |
Definition at line 617 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_sparc | ( | const irep_idt & | subarch | ) |
Definition at line 457 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_v850 | ( | ) |
Sets up the widths of variables for the Renesas V850.
Definition at line 565 of file config.cpp.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_x32 | ( | ) |
Definition at line 528 of file config.cpp.
References UNREACHABLE.
Referenced by configt::set_arch().
void configt::ansi_ct::set_arch_spec_x86_64 | ( | ) |
Definition at line 180 of file config.cpp.
References UNREACHABLE.
Referenced by gcc_modet::doit(), and configt::set_arch().
|
inline |
Definition at line 53 of file config.h.
References C11, c_standard, and for_has_scope.
Referenced by gcc_modet::doit(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), and goto_analyzer_parse_optionst::get_command_line_options().
|
inline |
Definition at line 51 of file config.h.
References C89, c_standard, and for_has_scope.
Referenced by gcc_modet::doit(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), and goto_analyzer_parse_optionst::get_command_line_options().
|
inline |
Definition at line 52 of file config.h.
References C99, c_standard, and for_has_scope.
Referenced by gcc_modet::doit(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), and goto_analyzer_parse_optionst::get_command_line_options().
void configt::ansi_ct::set_ILP32 | ( | ) |
int=32, long=32, pointer=32
Definition at line 109 of file config.cpp.
References alignment().
Referenced by configt::set().
void configt::ansi_ct::set_ILP64 | ( | ) |
int=64, long=64, pointer=64
Definition at line 69 of file config.cpp.
References alignment().
Referenced by configt::set().
void configt::ansi_ct::set_LLP64 | ( | ) |
int=32, long=32, pointer=64
Definition at line 89 of file config.cpp.
References alignment().
Referenced by configt::set().
void configt::ansi_ct::set_LP32 | ( | ) |
int=16, long=32, pointer=32
Definition at line 129 of file config.cpp.
References alignment().
Referenced by configt::set(), and set_16().
void configt::ansi_ct::set_LP64 | ( | ) |
int=32, long=64, pointer=64
Definition at line 45 of file config.cpp.
References alignment().
Referenced by configt::set().
|
static |
Definition at line 1052 of file config.cpp.
Referenced by configt::set_from_symbol_table().
std::size_t configt::ansi_ct::alignment |
Definition at line 69 of file config.h.
Referenced by add_padding_gcc(), ansi_c_architecture_strings(), and configt::set_from_symbol_table().
irep_idt configt::ansi_ct::arch |
Definition at line 84 of file config.h.
Referenced by ansi_c_architecture_strings(), ansi_c_internal_additions(), builtin_factory(), cpp_internal_additions(), armcc_modet::doit(), gcc_modet::doit(), goto_instrument_parse_optionst::instrument_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), configt::set(), and configt::set_arch().
std::size_t configt::ansi_ct::bool_width |
Definition at line 32 of file config.h.
Referenced by ansi_c_architecture_strings(), c_bool_type(), configt::set(), and configt::set_from_symbol_table().
enum configt::ansi_ct::c_standardt configt::ansi_ct::c_standard |
Referenced by c_preprocess_arm(), c_preprocess_gcc_clang(), gcc_modet::doit(), configt::set(), set_c11(), set_c89(), and set_c99().
bool configt::ansi_ct::char_is_unsigned |
Definition at line 43 of file config.h.
Referenced by ansi_c_architecture_strings(), c_preprocess_arm(), c_preprocess_gcc_clang(), c_preprocess_visual_studio(), char_type(), expr2ct::convert_rec(), ms_cl_modet::doit(), armcc_modet::doit(), gcc_modet::doit(), configt::set(), and configt::set_from_symbol_table().
std::size_t configt::ansi_ct::char_width |
Definition at line 33 of file config.h.
Referenced by add_padding(), add_padding_gcc(), add_padding_msvc(), ansi_c_architecture_strings(), char_type(), expr2ct::convert_rec(), c_typecheck_baset::enum_underlying_type(), c_typecastt::get_c_type(), string_abstractiont::is_char_type(), string_instrumentationt::is_string_type(), c_typecastt::minimum_promotion(), configt::set(), configt::set_from_symbol_table(), signed_char_type(), unsigned_char_type(), and xml().
|
static |
Definition at line 123 of file config.h.
Referenced by configt::set_object_bits_from_symbol_table().
std::list<std::string> configt::ansi_ct::defines |
Definition at line 112 of file config.h.
Referenced by compilet::add_compiler_specific_defines(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_visual_studio(), ms_cl_modet::doit(), armcc_modet::doit(), cw_modet::doit(), goto_instrument_parse_optionst::instrument_goto_program(), configt::set(), and configt::set_from_symbol_table().
std::size_t configt::ansi_ct::double_width |
Definition at line 38 of file config.h.
Referenced by ansi_c_architecture_strings(), expr2ct::convert_rec(), gcc_modet::doit(), c_typecastt::get_c_type(), configt::set(), and configt::set_from_symbol_table().
endiannesst configt::ansi_ct::endianness |
Definition at line 76 of file config.h.
Referenced by ansi_c_architecture_strings(), value_set_dereferencet::build_reference_to(), byte_extract_id(), byte_update_id(), c_preprocess_arm(), boolbvt::convert_union(), boolbvt::convert_with_union(), gcc_modet::doit(), value_set_dereferencet::memory_model_bytes(), configt::set(), configt::set_arch(), and configt::set_from_symbol_table().
bool configt::ansi_ct::Float128_type |
Definition at line 46 of file config.h.
Referenced by gcc_modet::doit(), ansi_c_languaget::parse(), and configt::set().
bool configt::ansi_ct::for_has_scope |
Definition at line 44 of file config.h.
Referenced by convert(), ansi_c_languaget::parse(), configt::set(), set_c11(), set_c89(), set_c99(), and c_typecheck_baset::typecheck_for().
std::list<std::string> configt::ansi_ct::include_files |
Definition at line 116 of file config.h.
Referenced by c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_visual_studio(), and configt::set().
std::list<std::string> configt::ansi_ct::include_paths |
Definition at line 115 of file config.h.
Referenced by c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_visual_studio(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), and configt::set().
std::size_t configt::ansi_ct::int_width |
Definition at line 30 of file config.h.
Referenced by ansi_c_architecture_strings(), c_preprocess_visual_studio(), goto_program2codet::cleanup_expr(), convert_integer_literal(), expr2ct::convert_rec(), cpp_convert_plain_type(), c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), generate_ansi_c_start_function(), c_typecastt::get_c_type(), c_typecastt::minimum_promotion(), pointer_diff_type(), configt::set(), configt::set_from_symbol_table(), signed_int_type(), signed_poly_type(), size_type(), cpp_typecheckt::standard_conversion_integral_promotion(), cpp_typecheckt::typecheck_expr_new(), unsigned_int_type(), unsigned_poly_type(), and xml().
libt configt::ansi_ct::lib |
Definition at line 119 of file config.h.
Referenced by cprover_c_library_factory(), cprover_cpp_library_factory(), configt::set(), and configt::set_arch().
std::size_t configt::ansi_ct::long_double_width |
Definition at line 39 of file config.h.
Referenced by ansi_c_architecture_strings(), expr2ct::convert_rec(), c_typecastt::get_c_type(), long_double_type(), configt::set(), and configt::set_from_symbol_table().
std::size_t configt::ansi_ct::long_int_width |
Definition at line 31 of file config.h.
Referenced by ansi_c_architecture_strings(), ansi_c_internal_additions(), convert_integer_literal(), expr2ct::convert_rec(), cpp_internal_additions(), c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), c_typecastt::get_c_type(), pointer_diff_type(), configt::set(), configt::set_from_symbol_table(), signed_long_int_type(), size_type(), c_typecheck_baset::typecheck_type(), unsigned_long_int_type(), and xml().
std::size_t configt::ansi_ct::long_long_int_width |
Definition at line 35 of file config.h.
Referenced by ansi_c_architecture_strings(), dump_ct::convert_compound(), convert_integer_literal(), expr2ct::convert_rec(), c_typecheck_baset::enum_constant_type(), c_typecastt::get_c_type(), pointer_diff_type(), configt::set(), configt::set_from_symbol_table(), signed_long_long_int_type(), size_type(), c_typecheck_baset::typecheck_type(), unsigned_long_long_int_type(), and xml().
std::size_t configt::ansi_ct::memory_operand_size |
Definition at line 73 of file config.h.
Referenced by ansi_c_architecture_strings(), print_struct_alignment_problems(), and configt::set_from_symbol_table().
flavourt configt::ansi_ct::mode |
Definition at line 106 of file config.h.
Referenced by add_padding(), ansi_c_internal_additions(), builtin_factory(), c_preprocess_gcc_clang(), c_preprocess_none(), convert(), expr2ct::convert_with_precedence(), cpp_internal_additions(), 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(), ansi_c_languaget::parse(), cpp_languaget::parse(), configt::set(), ansi_c_languaget::to_expr(), ansi_c_declarationt::to_symbol(), cpp_typecheckt::typecheck_enum_type(), and c_typecheck_baset::typecheck_redefinition_non_type().
bool configt::ansi_ct::NULL_is_zero |
Definition at line 87 of file config.h.
Referenced by ansi_c_architecture_strings(), expr2ct::convert_constant(), is_dereference_integer_object(), configt::set(), configt::set_arch(), configt::set_from_symbol_table(), simplify_exprt::simplify_inequality_constant(), simplify_json_expr(), and simplify_exprt::simplify_typecast().
ost configt::ansi_ct::os |
Definition at line 79 of file config.h.
Referenced by ansi_c_architecture_strings(), ansi_c_internal_additions(), builtin_factory(), c_preprocess_gcc_clang(), expr2ct::convert_code_decl(), cpp_internal_additions(), configt::set(), configt::set_from_symbol_table(), and c_typecheck_baset::typecheck_redefinition_type().
std::size_t configt::ansi_ct::pointer_width |
Definition at line 36 of file config.h.
Referenced by ansi_c_architecture_strings(), c_preprocess_gcc_clang(), c_preprocess_visual_studio(), configt::object_bits_info(), pointer_diff_type(), pointer_type(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), reference_type(), configt::set(), set_arch_spec_mips(), configt::set_from_symbol_table(), configt::set_object_bits_from_symbol_table(), and size_type().
preprocessort configt::ansi_ct::preprocessor |
Definition at line 110 of file config.h.
Referenced by c_preprocess(), c_typecheck_baset::do_special_functions(), model_argc_argv(), and configt::set().
std::list<std::string> configt::ansi_ct::preprocessor_options |
Definition at line 114 of file config.h.
Referenced by c_preprocess_codewarrior(), c_preprocess_gcc_clang(), ms_cl_modet::doit(), cw_modet::doit(), armcc_modet::doit(), and gcc_modet::doit().
ieee_floatt::rounding_modet configt::ansi_ct::rounding_mode |
Definition at line 55 of file config.h.
Referenced by ansi_c_internal_additions(), cpp_internal_additions(), and configt::set().
std::size_t configt::ansi_ct::short_int_width |
Definition at line 34 of file config.h.
Referenced by ansi_c_architecture_strings(), c_preprocess_gcc_clang(), expr2ct::convert_rec(), gcc_modet::doit(), c_typecheck_baset::enum_underlying_type(), c_typecastt::get_c_type(), c_typecastt::minimum_promotion(), configt::set(), configt::set_from_symbol_table(), signed_short_int_type(), unsigned_short_int_type(), and xml().
bool configt::ansi_ct::single_precision_constant |
Definition at line 47 of file config.h.
Referenced by convert_float_literal(), gcc_modet::doit(), and configt::set().
std::size_t configt::ansi_ct::single_width |
Definition at line 37 of file config.h.
Referenced by ansi_c_architecture_strings(), expr2ct::convert_rec(), gcc_modet::doit(), c_typecastt::get_c_type(), configt::set(), configt::set_from_symbol_table(), and cpp_typecheckt::standard_conversion_floating_point_promotion().
bool configt::ansi_ct::string_abstraction |
Definition at line 121 of file config.h.
Referenced by get_cprover_library_text(), and configt::set().
bool configt::ansi_ct::ts_18661_3_Floatn_types |
Definition at line 45 of file config.h.
Referenced by gcc_modet::doit(), ansi_c_languaget::parse(), configt::set(), and ansi_c_languaget::to_expr().
std::list<std::string> configt::ansi_ct::undefines |
Definition at line 113 of file config.h.
Referenced by armcc_modet::doit(), ms_cl_modet::doit(), cw_modet::doit(), and gcc_modet::doit().
bool configt::ansi_ct::wchar_t_is_unsigned |
Definition at line 43 of file config.h.
Referenced by ansi_c_architecture_strings(), gcc_modet::doit(), configt::set(), configt::set_from_symbol_table(), and wchar_t_type().
std::size_t configt::ansi_ct::wchar_t_width |
Definition at line 40 of file config.h.
Referenced by ansi_c_architecture_strings(), c_preprocess_gcc_clang(), armcc_modet::doit(), gcc_modet::doit(), configt::set(), configt::set_from_symbol_table(), and wchar_t_type().