cprover
messaget Class Reference

#include <message.h>

Inheritance diagram for messaget:
[legend]
Collaboration diagram for messaget:
[legend]

Classes

class  mstreamt
 

Public Types

enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Static Public Member Functions

static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Protected Attributes

message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 102 of file message.h.

Member Enumeration Documentation

◆ message_levelt

Enumerator
M_ERROR 
M_WARNING 
M_RESULT 
M_STATUS 
M_STATISTICS 
M_PROGRESS 
M_DEBUG 

Definition at line 116 of file message.h.

Constructor & Destructor Documentation

◆ messaget() [1/3]

messaget::messaget ( )
inline

Definition at line 135 of file message.h.

◆ messaget() [2/3]

messaget::messaget ( const messaget other)
inline

Definition at line 141 of file message.h.

◆ messaget() [3/3]

messaget::messaget ( message_handlert _message_handler)
inlineexplicit

Definition at line 147 of file message.h.

◆ ~messaget()

messaget::~messaget ( )
virtual

Definition at line 66 of file message.cpp.

Member Function Documentation

◆ debug()

mstreamt& messaget::debug ( )
inline

Definition at line 253 of file message.h.

References get_mstream(), and M_DEBUG.

Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), string_refinementt::add_instantiations(), string_refinementt::add_lemma(), shared_bufferst::affected_by_delay(), bv_refinementt::arrays_overapproximated(), as_modet::as_hybrid_binary(), gcc_modet::asm_output(), event_grapht::graph_explorert::backtrack(), string_refinementt::boolbv_set_equality_to_true(), string_refinementt::check_axioms(), bv_refinementt::check_SAT(), event_grapht::graph_pensieve_explorert::collect_pairs(), fence_all_sharedt::compute(), fence_volatilet::compute(), string_refinementt::compute_inverse_function(), instrumentert::cfg_visitort::contains_shared_array(), java_bytecode_convert_classt::convert(), compilet::convert_symbols(), bv_refinementt::dec_solve(), string_refinementt::dec_solve(), shared_bufferst::delay_read(), shared_bufferst::det_flush(), linkingt::detailed_conflict_report_rec(), string_refinementt::display_index_set(), cbmc_parse_optionst::do_bmc(), java_bytecode_languaget::do_ci_lazy_method_conversion(), linkingt::do_type_dependencies(), as_modet::doit(), gcc_modet::doit(), ms_cl_modet::doit(), armcc_modet::doit(), cw_modet::doit(), clobber_parse_optionst::doit(), symex_parse_optionst::doit(), compilet::doit(), path_searcht::drop_state(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), event_grapht::graph_explorert::filter_thin_air(), goto_convertt::finish_gotos(), gcc_modet::gcc_hybrid_binary(), string_refinementt::get_array(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), java_class_loadert::get_parse_tree(), fence_insertert::get_type(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), string_refinementt::instantiate_not_contains(), taint_analysist::instrument(), instrumentert::instrument_minimum_interference_inserter(), instrumentert::instrument_my_events(), instrumentert::instrument_with_strategy(), instrumentert::is_cfg_spurious(), instrumentert::local(), fence_insertert::mip_fill_matrix(), shared_bufferst::nondet_flush(), java_class_loadert::operator()(), taint_analysist::operator()(), path_searcht::operator()(), gcc_modet::preprocess(), data_dpt::print(), instrumentert::print_map_function_graph(), instrumentert::print_outputs(), instrumentert::print_outputs_local(), const_function_pointer_propagationt::propagate(), java_class_loadert::read_jar_file(), linkingt::rename_symbols(), fault_localizationt::report(), const_function_pointer_propagationt::resolve(), gcc_modet::run_gcc(), string_refinementt::set_mode(), fence_insertert::solve(), symex_bmct::symex_step(), linkingt::typecheck(), java_bytecode_languaget::typecheck(), shared_bufferst::unique(), string_refinementt::update_index_set(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_duplicate(), instrumentert::cfg_visitort::visit_cfg_reference_function(), shared_bufferst::cfg_visitort::weak_memory(), and shared_bufferst::write().

◆ endl()

static mstreamt& messaget::endl ( mstreamt m)
inlinestatic

◆ eom()

static mstreamt& messaget::eom ( mstreamt m)
inlinestatic

Definition at line 193 of file message.h.

References irept::clear(), message_handlert::flush(), messaget::mstreamt::message, message_handler, messaget::mstreamt::message_level, message_handlert::print(), and messaget::mstreamt::source_location.

Referenced by string_abstractiont::abstract_function_call(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), const_function_pointer_propagationt::arg_stackt::add_args(), cpp_typecheckt::add_base_components(), compilet::add_input_file(), string_refinementt::add_instantiations(), string_refinementt::add_lemma(), shared_bufferst::affected_by_delay(), ansi_c_entry_point(), ansi_c_typecheck(), c_typecheck_baset::apply_asm_label(), bv_refinementt::arrays_overapproximated(), as_modet::as_hybrid_binary(), gcc_modet::asm_output(), shared_bufferst::assignment(), event_grapht::graph_explorert::backtrack(), string_refinementt::boolbv_set_equality_to_true(), partial_order_concurrencyt::build_event_lists(), string_abstractiont::build_wrap(), c_preprocess(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_none(), c_preprocess_visual_studio(), instrumentert::cfg_cycles_filter(), path_searcht::check_assertion(), string_refinementt::check_axioms(), cpp_typecheckt::check_member_initializers(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), cpp_typecheckt::class_template_symbol(), goto_convertt::clean_expr(), event_grapht::graph_explorert::collect_cycles(), event_grapht::graph_pensieve_explorert::collect_pairs(), cpp_declarator_convertert::combine_types(), compilet::compile(), qbf_bdd_coret::compress_certificate(), fence_all_sharedt::compute(), fence_all_shared_aegt::compute(), fence_insertert::compute(), fence_volatilet::compute(), string_refinementt::compute_inverse_function(), aig_prop_solvert::compute_phase(), instrumentert::cfg_visitort::contains_shared_array(), cpp_declarator_convertert::convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), goto_convertt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assign(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_break(), boolbvt::convert_bv(), cpp_typecheckt::convert_class_template_specialization(), boolbvt::convert_constant(), goto_convertt::convert_continue(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), goto_convertt::convert_dowhile(), goto_convertt::convert_end_thread(), goto_convertt::convert_expression(), boolbvt::convert_extractbits(), goto_convert_functionst::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_ifthenelse(), goto_convertt::convert_init(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_convertt::convert_loop_invariant(), boolbvt::convert_member(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), cpp_typecheckt::convert_pmop(), boolbvt::convert_rest(), goto_convertt::convert_return(), goto_convertt::convert_specc_event(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), boolbvt::convert_struct(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), boolbvt::convert_symbol(), compilet::convert_symbols(), cpp_typecheckt::convert_template_declaration(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheck_resolvet::convert_template_parameter(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), boolbvt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), event_grapht::copy_segment(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheck(), bv_refinementt::dec_solve(), cvc_dect::dec_solve(), smt1_dect::dec_solve(), smt2_dect::dec_solve(), string_refinementt::dec_solve(), prop_conv_solvert::dec_solve(), shared_bufferst::delay_read(), c_typecheck_baset::designator_enter(), shared_bufferst::det_flush(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_template_classes(), string_refinementt::display_index_set(), goto_convertt::do_array_equal(), goto_convertt::do_array_op(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), cbmc_parse_optionst::do_bmc(), cpp_typecheck_resolvet::do_builtin(), java_bytecode_languaget::do_ci_lazy_method_conversion(), bmct::do_conversion(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_fscanf(), goto_convertt::do_function_call(), goto_convertt::do_function_call_symbol(), goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_input(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), goto_convertt::do_output(), goto_instrument_parse_optionst::do_partial_inlining(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), goto_instrument_parse_optionst::do_remove_const_function_pointers_only(), goto_instrument_parse_optionst::do_remove_returns(), goto_convertt::do_scanf(), path_searcht::do_show_vcc(), string_instrumentationt::do_snprintf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), linkingt::do_type_dependencies(), as_modet::doit(), gcc_modet::doit(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), goto_fence_inserter_parse_optionst::doit(), goto_diff_parse_optionst::doit(), clobber_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), symex_parse_optionst::doit(), compilet::doit(), cbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), path_searcht::drop_state(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), error_parse_line(), bmct::error_trace(), goto_inlinet::expand_function_call(), event_grapht::graph_explorert::extract_cycle(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), fence_pensieve(), fence_weak_memory(), event_grapht::graph_explorert::filter_thin_air(), language_uit::final(), compilet::find_library(), goto_convertt::finish_gotos(), cpp_typecheckt::full_member_initialization(), gcc_modet::gcc_hybrid_binary(), java_bytecode_convert_classt::generate_class_stub(), string_refinementt::get_array(), goto_convertt::get_array_argument(), java_bytecode_convert_methodt::get_bytecode_info(), qbf_skizzo_coret::get_certificate(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), goto_fence_inserter_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), get_main_symbol(), get_module(), get_module_by_name(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), java_class_loadert::get_parse_tree(), cbmc_solverst::get_smt1(), cbmc_solverst::get_smt2(), goto_convertt::get_string_constant(), fence_insertert::get_type(), instrumentert::goto2graph_cfg(), goto_convert(), goto_inlinet::goto_inline_transitive(), const_graph_visitort::graph_explore_AC(), const_graph_visitort::graph_explore_BC(), cpp_typecheck_resolvet::guess_function_template_args(), prop_conv_solvert::ignoring(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), initialize_goto_model(), goto_inlinet::insert_function_nobody(), string_refinementt::instantiate_not_contains(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), instrument_cover_goals(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), instrumentert::instrument_minimum_interference_inserter(), instrumentert::instrument_my_events(), instrumentert::instrument_with_strategy(), introduce_temporaries(), instrumentert::is_cfg_spurious(), path_searcht::is_feasible(), event_grapht::critical_cyclet::is_unsafe(), event_grapht::critical_cyclet::is_unsafe_asm(), java_bytecode_convert_class(), java_bytecode_parse(), java_entry_point(), jsil_convert(), jsil_entry_point(), jsil_typecheck(), static_analyzert::json_report(), compilet::link(), linkingt::link_error(), link_to_library(), linkingt::link_warning(), instrumentert::local(), goto_convertt::lookup(), goto_cc_modet::main(), cpp_declarator_convertert::main_function_rules(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), c_typecheck_baset::make_designator(), boolbvt::make_free_bv_expr(), jsil_typecheckt::make_type_compatible(), fence_insertert::mip_fill_matrix(), model_argc_argv(), cpp_typecheckt::move_member_initializers(), c_typecheck_baset::move_symbol(), cbmc_solverst::no_beautification(), symex_bmct::no_body(), cbmc_solverst::no_incremental_check(), shared_bufferst::nondet_flush(), jar_filet::open(), memory_model_psot::operator()(), memory_model_sct::operator()(), memory_model_tsot::operator()(), java_class_loadert::operator()(), jsil_convertt::operator()(), counterexample_beautificationt::operator()(), prop_minimizet::operator()(), bmc_all_propertiest::operator()(), cover_goalst::operator()(), static_analyzert::operator()(), taint_analysist::operator()(), path_searcht::operator()(), bmc_covert::operator()(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), language_uit::parse(), java_bytecode_parsert::parse(), java_bytecode_languaget::parse(), compilet::parse(), language_filest::parse(), parsert::parse_error(), compilet::parse_stdin(), pbs_dimacs_cnft::pbs_solve(), static_analyzert::plain_text_report(), java_bytecode_parsert::pool_entry(), java_bytecode_convert_methodt::pop(), populate_predecessor_map(), gcc_modet::preprocess(), fence_insertert::preprocess(), cbmc_parse_optionst::preprocessing(), data_dpt::print(), instrumentert::print_map_function_graph(), instrumentert::print_outputs(), instrumentert::print_outputs_local(), fence_insertert::print_to_file_3(), fence_insertert::print_to_file_4(), fence_insertert::print_vars(), goto_diff_parse_optionst::process_goto_program(), clobber_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), qbf_quantort::prop_solve(), qbf_qubet::prop_solve(), qbf_skizzot::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_limmatt::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_booleforce_baset::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_picosatt::prop_solve(), satcheck_smvsatt::prop_solve(), satcheck_precosatt::prop_solve(), satcheck_minisat1_baset::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_qube_coret::prop_solve(), qbf_squolemt::prop_solve(), qbf_squolem_coret::prop_solve(), pbs_dimacs_cnft::prop_solve(), qbf_bdd_coret::prop_solve(), aig_prop_solvert::prop_solve(), const_function_pointer_propagationt::propagate(), cpp_typecheckt::put_compound_into_scope(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rconstant_pool(), read_bin_goto_object(), java_bytecode_parsert::read_bytes(), cvc_dect::read_cvcl_result(), read_goto_binary(), read_goto_object(), java_class_loadert::read_jar_file(), read_object_and_link(), smt2_dect::read_result(), smt1_dect::read_result_boolector(), smt1_dect::read_result_yices(), cpp_typecheckt::reference_initializer(), const_function_pointer_propagationt::arg_stackt::remove_args(), goto_convertt::remove_assignment(), remove_function(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), remove_unused_functions(), linkingt::rename_symbols(), goto_inlinet::replace_return(), fault_localizationt::report(), bmc_all_propertiest::report(), symex_parse_optionst::report_cover(), clobber_parse_optionst::report_failure(), symex_parse_optionst::report_failure(), bmct::report_failure(), symex_parse_optionst::report_properties(), path_searcht::report_statistics(), clobber_parse_optionst::report_success(), symex_parse_optionst::report_success(), bmct::report_success(), cpp_typecheck_resolvet::resolve(), const_function_pointer_propagationt::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), bmct::run(), fault_localizationt::run(), bmct::run_decision_procedure(), fault_localizationt::run_decision_procedure(), gcc_modet::run_gcc(), bmc_covert::satisfying_assignment(), string_refinementt::set_mode(), symex_parse_optionst::set_properties(), goto_analyzer_parse_optionst::set_properties(), cbmc_parse_optionst::set_properties(), boolbvt::set_to(), language_uit::show_symbol_table(), language_uit::show_symbol_table_xml_ui(), bmct::show_vcc(), java_bytecode_parsert::skip_bytes(), skip_loops(), fence_insertert::solve(), fault_localizationt::stop_on_fail(), bmct::stop_on_fail(), symex_bmct::symex_step(), Parser::SyntaxError(), taint_parser(), cpp_typecheckt::template_suffix(), language_uit::typecheck(), linkingt::typecheck(), java_bytecode_languaget::typecheck(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_assign(), cpp_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_break(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_class_template_member(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_continue(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_dowhile(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), jsil_typecheckt::typecheck_exp_binary_equal(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_num(), jsil_typecheckt::typecheck_expr_unary_string(), c_typecheck_baset::typecheck_expression(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_gcc_computed_goto(), c_typecheck_baset::typecheck_gcc_switch_case_range(), c_typecheck_baset::typecheck_ifthenelse(), typecheckt::typecheck_main(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), language_filest::typecheck_module(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), c_typecheck_baset::typecheck_switch(), c_typecheck_baset::typecheck_switch_case(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), jsil_typecheckt::typecheck_try_catch(), java_bytecode_typecheckt::typecheck_type(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), c_typecheck_baset::typecheck_while(), shared_bufferst::unique(), jsil_typecheckt::update_expr_type(), string_refinementt::update_index_set(), aig_prop_solvert::usage_count(), instrumentert::cfg_visitort::visit_cfg(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_backedge(), instrumentert::cfg_visitort::visit_cfg_duplicate(), instrumentert::cfg_visitort::visit_cfg_fence(), instrumentert::cfg_visitort::visit_cfg_function(), instrumentert::cfg_visitort::visit_cfg_function_call(), instrumentert::cfg_visitort::visit_cfg_goto(), instrumentert::cfg_visitort::visit_cfg_lwfence(), instrumentert::cfg_visitort::visit_cfg_reference_function(), weak_memory(), shared_bufferst::cfg_visitort::weak_memory(), ansi_c_convert_typet::write(), shared_bufferst::write(), compilet::write_bin_object_file(), cbmc_dimacst::write_dimacs(), static_analyzert::xml_report(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

◆ error()

mstreamt& messaget::error ( )
inline

Definition at line 223 of file message.h.

References get_mstream(), and M_ERROR.

Referenced by string_abstractiont::abstract_function_call(), cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), cpp_typecheckt::add_base_components(), compilet::add_input_file(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), as_modet::as_hybrid_binary(), gcc_modet::asm_output(), c_preprocess(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_none(), c_preprocess_visual_studio(), cpp_typecheckt::check_member_initializers(), cpp_typecheckt::class_template_symbol(), goto_convertt::clean_expr(), cpp_declarator_convertert::combine_types(), cpp_declarator_convertert::convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), goto_convertt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assign(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_break(), boolbvt::convert_bv(), cpp_typecheckt::convert_class_template_specialization(), boolbvt::convert_constant(), goto_convertt::convert_continue(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), goto_convertt::convert_dowhile(), goto_convertt::convert_end_thread(), goto_convertt::convert_expression(), boolbvt::convert_extractbits(), goto_convert_functionst::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_ifthenelse(), goto_convertt::convert_init(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_convertt::convert_loop_invariant(), boolbvt::convert_member(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_parameter(), cpp_typecheckt::convert_pmop(), boolbvt::convert_rest(), goto_convertt::convert_return(), goto_convertt::convert_specc_event(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), boolbvt::convert_struct(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), boolbvt::convert_symbol(), cpp_typecheckt::convert_template_declaration(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheck_resolvet::convert_template_parameter(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), boolbvt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), smt1_dect::dec_solve(), smt2_dect::dec_solve(), c_typecheck_baset::designator_enter(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_template_classes(), goto_convertt::do_array_equal(), goto_convertt::do_array_op(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_fscanf(), goto_convertt::do_function_call(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_input(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), goto_convertt::do_output(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), as_modet::doit(), gcc_modet::doit(), goto_fence_inserter_parse_optionst::doit(), goto_diff_parse_optionst::doit(), clobber_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), symex_parse_optionst::doit(), compilet::doit(), cbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), typecheckt::err_location(), error_parse_line(), language_uit::final(), goto_convertt::finish_gotos(), cpp_typecheckt::full_member_initialization(), gcc_modet::gcc_hybrid_binary(), goto_convertt::get_array_argument(), java_bytecode_convert_methodt::get_bytecode_info(), qbf_skizzo_coret::get_certificate(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), cpp_typecheckt::get_component(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), get_main_symbol(), get_module(), get_module_by_name(), cbmc_solverst::get_smt1(), cbmc_solverst::get_smt2(), goto_convertt::get_string_constant(), goto_convert(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_declarator_convertert::handle_initializer(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), initialize_goto_model(), cpp_typecheckt::instantiate_template(), instrument_cover_goals(), goto_instrument_parse_optionst::instrument_goto_program(), java_bytecode_parse(), java_entry_point(), jsil_entry_point(), static_analyzert::json_report(), linkingt::link_error(), goto_convertt::lookup(), goto_cc_modet::main(), cpp_declarator_convertert::main_function_rules(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), c_typecheck_baset::make_designator(), boolbvt::make_free_bv_expr(), jsil_typecheckt::make_type_compatible(), model_argc_argv(), cpp_typecheckt::move_member_initializers(), c_typecheck_baset::move_symbol(), cbmc_solverst::no_beautification(), cbmc_solverst::no_incremental_check(), jsil_convertt::operator()(), prop_minimizet::operator()(), bmc_all_propertiest::operator()(), cover_goalst::operator()(), taint_analysist::operator()(), path_searcht::operator()(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), language_uit::parse(), java_bytecode_parsert::parse(), compilet::parse(), language_filest::parse(), parsert::parse_error(), compilet::parse_stdin(), pbs_dimacs_cnft::pbs_solve(), java_bytecode_parsert::pool_entry(), java_bytecode_convert_methodt::pop(), cbmc_parse_optionst::preprocessing(), goto_diff_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), qbf_qubet::prop_solve(), qbf_skizzot::prop_solve(), qbf_quantort::prop_solve(), qbf_skizzo_coret::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), cpp_typecheckt::put_compound_into_scope(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rconstant_pool(), read_bin_goto_object(), java_bytecode_parsert::read_bytes(), cvc_dect::read_cvcl_result(), dplib_dect::read_dplib_result(), read_goto_binary(), read_goto_object(), java_class_loadert::read_jar_file(), smt2_dect::read_result(), smt1_dect::read_result_boolector(), smt1_dect::read_result_yices(), cpp_typecheckt::reference_initializer(), goto_convertt::remove_assignment(), remove_function(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), goto_inlinet::replace_return(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), bmct::run(), goto_analyzer_parse_optionst::set_properties(), symex_parse_optionst::set_properties(), cbmc_parse_optionst::set_properties(), boolbvt::set_to(), language_uit::show_symbol_table(), language_uit::show_symbol_table_xml_ui(), bmct::show_vcc(), java_bytecode_parsert::skip_bytes(), skip_loops(), fault_localizationt::stop_on_fail(), bmct::stop_on_fail(), Parser::SyntaxError(), taint_parser(), cpp_typecheckt::template_suffix(), language_uit::typecheck(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_assign(), cpp_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_break(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_class_template_member(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_continue(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_dowhile(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), jsil_typecheckt::typecheck_exp_binary_equal(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_num(), jsil_typecheckt::typecheck_expr_unary_string(), c_typecheck_baset::typecheck_expression(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_gcc_computed_goto(), c_typecheck_baset::typecheck_gcc_switch_case_range(), c_typecheck_baset::typecheck_ifthenelse(), typecheckt::typecheck_main(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), language_filest::typecheck_module(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), c_typecheck_baset::typecheck_switch(), c_typecheck_baset::typecheck_switch_case(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), jsil_typecheckt::typecheck_try_catch(), java_bytecode_typecheckt::typecheck_type(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), c_typecheck_baset::typecheck_while(), jsil_typecheckt::update_expr_type(), ansi_c_convert_typet::write(), compilet::write_bin_object_file(), cbmc_dimacst::write_dimacs(), write_goto_binary(), static_analyzert::xml_report(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

◆ get_message_handler()

message_handlert& messaget::get_message_handler ( )
inline

Definition at line 127 of file message.h.

References INVARIANT, and message_handler.

Referenced by bmct::all_properties(), path_searcht::check_assertion(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_languaget::convert_lazy_method(), compilet::convert_symbols(), bmct::cover(), bmct::decide(), java_bytecode_languaget::do_ci_lazy_method_conversion(), c_typecheck_baset::do_designated_initializer(), goto_convertt::do_function_call_symbol(), goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), goto_instrument_parse_optionst::do_remove_const_function_pointers_only(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), goto_fence_inserter_parse_optionst::doit(), goto_diff_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), symex_parse_optionst::doit(), compilet::doit(), goto_instrument_parse_optionst::doit(), fault_localizationt::fault_localizationt(), ansi_c_languaget::final(), jsil_languaget::final(), cpp_languaget::final(), java_bytecode_languaget::final(), java_bytecode_convert_methodt::find_initialisers_for_slot(), cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_default(), cbmc_solverst::get_dimacs(), goto_fence_inserter_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), java_bytecode_languaget::get_language_options(), java_class_loadert::get_parse_tree(), cbmc_solverst::get_smt1(), cbmc_solverst::get_smt2(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), jsil_languaget::interfaces(), path_searcht::is_feasible(), compilet::link(), bv_minimizing_dect::minimize(), java_class_loadert::operator()(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), bv_minimizet::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), jar_poolt::operator()(), ansi_c_languaget::parse(), cpp_languaget::parse(), jsil_languaget::parse(), cpp_parsert::parse(), language_uit::parse(), java_bytecode_languaget::parse(), compilet::parse(), compilet::parse_stdin(), ansi_c_languaget::preprocess(), cpp_languaget::preprocess(), cbmc_parse_optionst::preprocessing(), goto_diff_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), remove_function_pointerst::remove_function_pointer(), bmct::run(), bmct::run_decision_procedure(), fault_localizationt::run_decision_procedure(), java_class_loadert::set_java_cp_include_files(), java_class_loader_limitt::setup_class_load_limit(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), ansi_c_languaget::typecheck(), jsil_languaget::typecheck(), cpp_languaget::typecheck(), java_bytecode_languaget::typecheck(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_type(), and cpp_typecheckt::zero_initializer().

◆ get_mstream()

mstreamt& messaget::get_mstream ( unsigned  message_level)
inline

Definition at line 217 of file message.h.

References messaget::mstreamt::message_level, and mstream.

Referenced by debug(), error(), progress(), result(), statistics(), status(), and warning().

◆ progress()

◆ result()

mstreamt& messaget::result ( )
inline

Definition at line 233 of file message.h.

References get_mstream(), and M_RESULT.

Referenced by linkingt::adjust_object_type(), linkingt::adjust_object_type_rec(), as_modet::as_hybrid_binary(), property_checkert::as_string(), gcc_modet::asm_output(), dplib_convt::bin_zero(), cvc_convt::bin_zero(), string_abstractiont::build(), string_abstractiont::build_unknown(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_unbounded_array(), smt1_convt::ce_value(), bv_refinementt::check_SAT(), java_class_loadert::class_name_to_file(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), fence_insertert::compute(), prop_conv_solvert::convert(), java_bytecode_convert_methodt::convert(), character_refine_preprocesst::convert_char_function(), character_refine_preprocesst::convert_compare(), character_refine_preprocesst::convert_digit_char(), character_refine_preprocesst::convert_for_digit(), goto_difft::convert_function(), goto_difft::convert_function_group(), smt2_convt::convert_identifier(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), character_refine_preprocesst::convert_is_ideographic(), character_refine_preprocesst::convert_is_ISO_control_char(), character_refine_preprocesst::convert_is_low_surrogate(), character_refine_preprocesst::convert_is_surrogate_pair(), boolbvt::convert_overflow(), character_refine_preprocesst::convert_to_code_point(), bv_cbmct::convert_waitfor_symbol(), prop_conv_solvert::dec_solve(), cbmc_parse_optionst::do_bmc(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), path_searcht::do_show_vcc(), goto_analyzer_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), equalityt::equality2(), bmct::error_trace(), qbf_bdd_certificatet::f_get(), java_class_loadert::file_to_class_name(), cpp_typecheckt::function_identifier(), gcc_modet::gcc_hybrid_binary(), cpp_enum_typet::generate_anon_tag(), prop_conv_solvert::get_bool(), qbf_skizzo_coret::get_certificate(), prop_conv_solvert::get_literal(), goto_convertt::get_string_constant(), cnf_clause_listt::hash(), qdimacs_cnft::hash(), cnf_clause_listt::hash_clause(), goto_instrument_parse_optionst::instrument_goto_program(), path_searcht::is_feasible(), satcheck_limmatt::l_get(), satcheck_booleforce_baset::l_get(), satcheck_picosatt::l_get(), satcheck_lingelingt::l_get(), satcheck_precosatt::l_get(), satcheck_smvsatt::l_get(), satcheck_minisat1_baset::l_get(), satcheck_zchaff_baset::l_get(), prop_conv_solvert::literal(), c_typecheck_baset::make_already_typechecked(), goto_convertt::make_compound_literal(), string_abstractiont::member(), propt::new_variables(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), bmct::output_graphml(), ansi_c_languaget::parse(), jsil_languaget::parse(), cpp_languaget::parse(), language_uit::parse(), smt2_convt::parse_struct(), static_analyzert::plain_text_report(), qbf_quantort::prop_solve(), qbf_skizzot::prop_solve(), qbf_qubet::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_booleforce_baset::prop_solve(), satcheck_smvsatt::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_qube_coret::prop_solve(), qbf_squolemt::prop_solve(), qbf_squolem_coret::prop_solve(), satcheck_smvsat_coret::prop_solve(), bv_refinementt::prop_solve(), pbs_dimacs_cnft::prop_solve(), java_bytecode_parsert::read_bytes(), bmc_all_propertiest::report(), symex_parse_optionst::report_cover(), clobber_parse_optionst::report_failure(), symex_parse_optionst::report_failure(), bmct::report_failure(), clobber_parse_optionst::report_success(), symex_parse_optionst::report_success(), bmct::report_success(), prop_conv_solvert::set_equality_to_true(), java_bytecode_convert_methodt::setup_local_variables(), fence_insertert::solve(), smt1_dect::string_to_expr_z3(), cpp_typecheckt::template_suffix(), java_bytecode_convert_methodt::tmp_variable(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), java_bytecode_languaget::to_expr(), linkingt::type_to_string_verbose(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_template_args(), c_typecheck_baset::typecheck_type(), java_bytecode_convert_methodt::variable(), and zero_initializert::zero_initializer_rec().

◆ set_message_handler()

virtual void messaget::set_message_handler ( message_handlert _message_handler)
inlinevirtual

Reimplemented in aig_prop_solvert.

Definition at line 122 of file message.h.

References message_handler.

Referenced by add_library(), bmct::all_properties(), ansi_c_entry_point(), path_searcht::check_assertion(), mmcc_parse_optionst::convert(), bmct::cover(), bmct::decide(), symex_parse_optionst::doit(), fault_localizationt::fault_localizationt(), language_uit::final(), cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_default(), cbmc_solverst::get_dimacs(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), cbmc_solverst::get_smt1(), cbmc_solverst::get_smt2(), initialize_goto_model(), path_searcht::is_feasible(), java_bytecode_parse(), jsil_entry_point(), language_uit::language_uit(), bv_minimizing_dect::minimize(), model_argc_argv(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), bv_minimizet::operator()(), bmc_covert::operator()(), jar_poolt::operator()(), ansi_c_languaget::parse(), jsil_languaget::parse(), cpp_languaget::parse(), cpp_parsert::parse(), language_uit::parse(), java_bytecode_languaget::parse(), compilet::parse(), parse_json(), compilet::parse_stdin(), parse_xml(), cbmc_parse_optionst::preprocessing(), read_goto_object(), bmct::run(), bmct::run_decision_procedure(), fault_localizationt::run_decision_procedure(), java_class_loadert::set_java_cp_include_files(), aig_prop_solvert::set_message_handler(), to_expr(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), and language_uit::typecheck().

◆ statistics()

◆ status()

mstreamt& messaget::status ( )
inline

Definition at line 238 of file message.h.

References get_mstream(), and M_STATUS.

Referenced by instrumentert::cfg_cycles_filter(), path_searcht::check_assertion(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), compilet::compile(), qbf_bdd_coret::compress_certificate(), fence_all_shared_aegt::compute(), fence_insertert::compute(), satcheck_zchaff_baset::copy_cnf(), event_grapht::copy_segment(), bv_refinementt::dec_solve(), cvc_dect::dec_solve(), dplib_dect::dec_solve(), bmct::do_conversion(), goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(), goto_instrument_parse_optionst::do_partial_inlining(), goto_instrument_parse_optionst::do_remove_const_function_pointers_only(), goto_instrument_parse_optionst::do_remove_returns(), as_modet::doit(), goto_fence_inserter_parse_optionst::doit(), goto_diff_parse_optionst::doit(), clobber_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), cbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), bmct::error_trace(), fence_pensieve(), fence_weak_memory(), java_bytecode_convert_methodt::find_initialisers_for_slot(), goto_fence_inserter_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), get_module(), instrumentert::goto2graph_cfg(), initialize_goto_model(), instrument_cover_goals(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), path_searcht::is_feasible(), static_analyzert::json_report(), satcheck_booleforce_baset::l_get(), satcheck_smvsatt::l_get(), satcheck_zchaff_baset::l_get(), link_to_library(), jar_filet::open(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), prop_minimizet::operator()(), static_analyzert::operator()(), taint_analysist::operator()(), path_searcht::operator()(), bmc_covert::operator()(), language_uit::parse(), java_bytecode_languaget::parse(), pbs_dimacs_cnft::pbs_solve(), static_analyzert::plain_text_report(), fence_insertert::preprocess(), clobber_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), qbf_quantort::prop_solve(), qbf_qubet::prop_solve(), qbf_skizzot::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_limmatt::prop_solve(), satcheck_booleforce_baset::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_picosatt::prop_solve(), satcheck_precosatt::prop_solve(), satcheck_smvsatt::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_minisat1_baset::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_squolem_coret::prop_solve(), qbf_squolemt::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), pbs_dimacs_cnft::prop_solve(), qbf_bdd_coret::prop_solve(), satcheck_minisat1_coret::prop_solve(), aig_prop_solvert::prop_solve(), remove_function(), fault_localizationt::report(), bmc_all_propertiest::report(), symex_parse_optionst::report_cover(), symex_parse_optionst::report_properties(), path_searcht::report_statistics(), bmct::run(), fault_localizationt::run(), bmct::run_decision_procedure(), fault_localizationt::run_decision_procedure(), satcheck_zchaff_baset::satcheck_zchaff_baset(), bmc_covert::satisfying_assignment(), fault_localizationt::stop_on_fail(), language_uit::typecheck(), language_filest::typecheck_module(), weak_memory(), and static_analyzert::xml_report().

◆ warning()

mstreamt& messaget::warning ( )
inline

Definition at line 228 of file message.h.

References get_mstream(), and M_WARNING.

Referenced by compilet::add_input_file(), shared_bufferst::assignment(), string_abstractiont::build_wrap(), event_grapht::graph_pensieve_explorert::collect_pairs(), compilet::compile(), fence_all_sharedt::compute(), fence_volatilet::compute(), cpp_typecheck_resolvet::do_builtin(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_list(), as_modet::doit(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), error_parse_line(), goto_inlinet::expand_function_call(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), compilet::find_library(), java_bytecode_convert_classt::generate_class_stub(), java_class_loadert::get_parse_tree(), prop_conv_solvert::ignoring(), c_typecheck_baset::implicit_typecast(), goto_inlinet::insert_function_nobody(), linkingt::link_warning(), model_argc_argv(), symex_bmct::no_body(), shared_bufferst::nondet_flush(), goto_inlinet::parameter_assignments(), populate_predecessor_map(), fence_insertert::print_to_file_3(), fence_insertert::print_to_file_4(), remove_function(), remove_function_pointerst::remove_function_pointer(), goto_inlinet::replace_return(), java_bytecode_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_function_call_arguments(), c_typecheck_baset::typecheck_ifthenelse(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_function_call(), instrumentert::cfg_visitort::visit_cfg(), and shared_bufferst::cfg_visitort::weak_memory().

Member Data Documentation

◆ message_handler

◆ mstream

mstreamt messaget::mstream
protected

Definition at line 260 of file message.h.

Referenced by get_mstream().


The documentation for this class was generated from the following files: