cprover
|
#include <message.h>
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_handlert & | get_message_handler () |
messaget () | |
messaget (const messaget &other) | |
messaget & | operator= (const messaget &other) |
messaget (message_handlert &_message_handler) | |
virtual | ~messaget () |
mstreamt & | get_mstream (unsigned message_level) const |
mstreamt & | error () const |
mstreamt & | warning () const |
mstreamt & | result () const |
mstreamt & | status () const |
mstreamt & | statistics () const |
mstreamt & | progress () const |
mstreamt & | debug () const |
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream . More... | |
Static Public Member Functions | |
static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More... | |
static mstreamt & | eom (mstreamt &m) |
static mstreamt & | endl (mstreamt &m) |
Protected Attributes | |
message_handlert * | message_handler |
mstreamt | mstream |
|
inlineexplicit |
|
virtual |
Definition at line 68 of file message.cpp.
void messaget::conditional_output | ( | mstreamt & | mstream, |
const std::function< void(mstreamt &)> & | output_generator | ||
) | const |
Generate output to mstream
using output_generator
if the configured verbosity is at least as high as that of mstream
.
Use whenever generating output involves additional computational effort that should only be spent when such output will actually be displayed.
mstream | Output message stream |
output_generator | Function generating output |
Definition at line 113 of file message.cpp.
References message_handlert::get_verbosity(), message_handler, messaget::mstreamt::message_level, and mstream.
Referenced by symex_target_equationt::convert_assignments(), symex_target_equationt::convert_assumptions(), symex_target_equationt::convert_constraints(), symex_target_equationt::convert_goto_instructions(), symex_target_equationt::convert_guards(), goto_symext::phi_function(), remove_function_pointerst::remove_function_pointer(), goto_symext::symex_assign_symbol(), and goto_symext::symex_goto().
|
inline |
Definition at line 332 of file message.h.
References get_mstream(), and M_DEBUG.
Referenced by compilet::add_files_from_archive(), compilet::add_input_file(), 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(), bv_refinementt::check_SAT(), event_grapht::graph_pensieve_explorert::collect_pairs(), instrumentert::cfg_visitort::contains_shared_array(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), ci_lazy_methodst::convert_and_analyze_method(), symex_target_equationt::convert_assignments(), symex_target_equationt::convert_assumptions(), symex_target_equationt::convert_constraints(), symex_target_equationt::convert_goto_instructions(), symex_target_equationt::convert_guards(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), compilet::convert_symbols(), bv_refinementt::dec_solve(), string_refinementt::dec_solve(), shared_bufferst::delay_read(), shared_bufferst::det_flush(), linkingt::detailed_conflict_report_rec(), linkingt::do_type_dependencies(), as_modet::doit(), ms_cl_modet::doit(), armcc_modet::doit(), cw_modet::doit(), gcc_modet::doit(), clobber_parse_optionst::doit(), compilet::doit(), event_grapht::graph_explorert::filter_thin_air(), goto_convertt::finish_gotos(), gcc_modet::gcc_hybrid_binary(), string_refinementt::get(), java_class_loadert::get_class_from_jar(), linker_script_merget::get_linker_script_data(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), java_class_loadert::get_parse_tree(), hybrid_binary(), taint_analysist::instrument(), instrumentert::instrument_minimum_interference_inserter(), instrumentert::instrument_my_events(), instrumentert::instrument_with_strategy(), instrumentert::is_cfg_spurious(), ld_modet::ld_hybrid_binary(), instrumentert::local(), shared_bufferst::nondet_flush(), taint_analysist::operator()(), java_class_loadert::operator()(), ci_lazy_methodst::operator()(), goto_symext::phi_function(), linker_script_merget::pointerize_linker_defined_symbols(), populate_predecessor_map(), gcc_modet::preprocess(), data_dpt::print(), instrumentert::print_map_function_graph(), interpretert::print_memory(), instrumentert::print_outputs(), instrumentert::print_outputs_local(), java_bytecode_parsert::read_bootstrapmethods_entry(), java_class_loadert::read_jar_file(), remove_function_pointerst::remove_function_pointer(), linkingt::rename_symbols(), linker_script_merget::replace_expr(), fault_localizationt::report(), fault_localizationt::report_xml(), gcc_modet::run_gcc(), ld_modet::run_ld(), java_bytecode_convert_methodt::setup_local_variables(), goto_symext::symex_assign_symbol(), goto_symext::symex_goto(), symex_bmct::symex_step(), linkingt::typecheck(), shared_bufferst::unique(), 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().
Definition at line 290 of file message.h.
Referenced by clobber_parse_optionst::doit().
Definition at line 272 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(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_format_specifier(), cpp_typecheckt::add_base_components(), compilet::add_files_from_archive(), compilet::add_input_file(), string_refinementt::add_lemma(), linker_script_merget::add_linker_script_definitions(), compilet::add_written_cprover_symbols(), 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(), interpretert::assign(), shared_bufferst::assignment(), event_grapht::graph_explorert::backtrack(), smt2_parsert::binary(), smt2_parsert::binary_predicate(), partial_order_concurrencyt::build_event_lists(), languaget::build_stub_parameter_symbol(), string_abstractiont::build_wrap(), c_preprocess(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_none(), c_preprocess_visual_studio(), smt2_parsert::cast_bv_to_signed(), smt2_parsert::cast_bv_to_unsigned(), instrumentert::cfg_cycles_filter(), check_axioms(), cpp_typecheckt::check_member_initializers(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), cpp_typecheckt::class_template_symbol(), goto_convertt::clean_expr(), arrayst::collect_arrays(), event_grapht::graph_explorert::collect_cycles(), event_grapht::graph_pensieve_explorert::collect_pairs(), cpp_declarator_convertert::combine_types(), smt2_parsert::command(), interpretert::command(), smt2_parsert::command_sequence(), compilet::compile(), qbf_bdd_coret::compress_certificate(), compute_inverse_function(), aig_prop_solvert::compute_phase(), interpretert::concretize_type(), instrumentert::cfg_visitort::contains_shared_array(), cpp_declarator_convertert::convert(), convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), goto_convertt::convert(), ci_lazy_methodst::convert_and_analyze_method(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assign(), symex_target_equationt::convert_assignments(), symex_target_equationt::convert_assumptions(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), goto_convertt::convert_break(), boolbvt::convert_bv(), cpp_typecheckt::convert_class_template_specialization(), boolbvt::convert_constant(), symex_target_equationt::convert_constraints(), 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(), symex_target_equationt::convert_goto_instructions(), symex_target_equationt::convert_guards(), goto_convertt::convert_ifthenelse(), goto_convertt::convert_init(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), 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(), goto_convertt::convert_return(), boolbvt::convert_struct(), 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(), 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(), create_stub_global_symbols(), debug_model(), bv_refinementt::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(), display_index_set(), goto_convertt::do_array_op(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), cpp_typecheck_resolvet::do_builtin(), 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(), bmct::do_language_agnostic_bmc(), 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(), 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(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), gcc_modet::doit(), clobber_parse_optionst::doit(), jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), compilet::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), error_parse_line(), bmct::error_trace(), interpretert::evaluate(), interpretert::evaluate_address(), bmct::execute(), interpretert::execute_assert(), interpretert::execute_assign(), interpretert::execute_function_call(), interpretert::execute_other(), goto_inlinet::expand_function_call(), smt2_parsert::expression(), event_grapht::graph_explorert::extract_cycle(), event_grapht::graph_explorert::filter_thin_air(), language_uit::final(), lazy_goto_modelt::finalize(), compilet::find_library(), goto_convertt::finish_gotos(), cpp_typecheckt::full_member_initialization(), smt2_parsert::function_application(), smt2_parsert::function_signature_declaration(), smt2_parsert::function_signature_definition(), gcc_modet::gcc_hybrid_binary(), generate_ansi_c_start_function(), generate_class_stub(), generate_function_bodies(), generate_function_bodies_factory(), generate_java_start_function(), generate_symbol_resolution_from_equations(), get_array(), goto_convertt::get_array_argument(), java_bytecode_convert_methodt::get_bytecode_info(), qbf_skizzo_coret::get_certificate(), get_char_array_and_concretize(), java_class_loadert::get_class_from_jar(), 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(), cpp_typecheckt::get_component(), get_cover_config(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), jbmc_parse_optionst::get_goto_program(), linker_script_merget::get_linker_script_data(), get_main_symbol(), bmct::get_memory_model(), get_module(), get_module_by_name(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), java_class_loadert::get_parse_tree(), java_string_library_preprocesst::get_primitive_value_of_object(), smt2_tokenizert::get_quoted_symbol(), cbmc_solverst::get_smt2(), goto_convertt::get_string_constant(), smt2_tokenizert::get_string_literal(), symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), interpretert::get_value(), instrumentert::goto2graph_cfg(), linker_script_merget::goto_and_object_mismatch(), goto_convert(), goto_inlinet::goto_inline_transitive(), cpp_typecheck_resolvet::guess_function_template_args(), havoc_generate_function_bodiest::havoc_expr_rec(), hybrid_binary(), smt2_parsert::ignore_command(), prop_conv_solvert::ignoring(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), lazy_goto_modelt::initialize(), initialize_goto_model(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), instrument_cover_goals(), 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(), event_grapht::critical_cyclet::is_unsafe(), event_grapht::critical_cyclet::is_unsafe_asm(), string_constraintt::is_valid_string_constraint(), java_bytecode_parse(), jsil_convert(), jsil_entry_point(), jsil_typecheck(), messaget::mstreamt::json_stream(), ld_modet::ld_hybrid_binary(), smt2_parsert::let_expression(), compilet::link(), linkingt::link_error(), linkingt::link_warning(), instrumentert::local(), 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(), jsil_typecheckt::make_type_compatible(), member_type_lazy(), model_argc_argv(), cpp_typecheckt::move_member_initializers(), c_typecheck_baset::move_symbol(), smt2_parsert::multi_ary(), smt2_tokenizert::next_token(), cbmc_solverst::no_beautification(), symex_bmct::no_body(), cbmc_solverst::no_incremental_check(), shared_bufferst::nondet_flush(), memory_model_tsot::operator()(), memory_model_sct::operator()(), memory_model_psot::operator()(), counterexample_beautificationt::operator()(), jsil_convertt::operator()(), bmc_all_propertiest::operator()(), cover_goalst::operator()(), prop_minimizet::operator()(), taint_analysist::operator()(), java_class_loadert::operator()(), interpretert::operator()(), bmc_covert::operator()(), ci_lazy_methodst::operator()(), messaget::mstreamt::operator<<(), goto_difft::output_functions(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), smt2irept::parse(), language_uit::parse(), java_bytecode_parsert::parse(), compilet::parse(), java_bytecode_languaget::parse(), language_filest::parse(), parsert::parse_error(), compilet::parse_stdin(), pbs_dimacs_cnft::pbs_solve(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), goto_symext::phi_function(), linker_script_merget::pointerize_linker_defined_symbols(), linker_script_merget::pointerize_subexprs_of(), java_bytecode_parsert::pool_entry(), java_bytecode_convert_methodt::pop(), populate_predecessor_map(), gcc_modet::preprocess(), cbmc_parse_optionst::preprocessing(), data_dpt::print(), instrumentert::print_map_function_graph(), interpretert::print_memory(), instrumentert::print_outputs(), instrumentert::print_outputs_local(), jbmc_parse_optionst::process_goto_function(), jbmc_parse_optionst::process_goto_functions(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), qbf_qubet::prop_solve(), qbf_skizzot::prop_solve(), qbf_quantort::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_booleforce_baset::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_picosatt::prop_solve(), satcheck_lingelingt::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_minisat1_baset::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_squolemt::prop_solve(), qbf_squolem_coret::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), pbs_dimacs_cnft::prop_solve(), qbf_bdd_coret::prop_solve(), aig_prop_solvert::prop_solve(), cpp_typecheckt::put_compound_into_scope(), smt2_parsert::quantifier_expression(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rClassFile(), java_bytecode_parsert::rconstant_pool(), read_bin_goto_object(), java_bytecode_parsert::read_bootstrapmethods_entry(), java_bytecode_parsert::read_bytes(), read_goto_binary(), java_class_loadert::read_jar_file(), read_object_and_link(), smt2_dect::read_result(), arrayst::record_array_equality(), cpp_typecheckt::reference_initializer(), 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(), linker_script_merget::replace_expr(), goto_inlinet::replace_return(), fault_localizationt::report(), bmc_all_propertiest::report(), cover_basic_blockst::report_block_anomalies(), clobber_parse_optionst::report_failure(), bmct::report_failure(), clobber_parse_optionst::report_success(), bmct::report_success(), fault_localizationt::report_xml(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), fault_localizationt::run(), fault_localizationt::run_decision_procedure(), bmct::run_decision_procedure(), gcc_modet::run_gcc(), ld_modet::run_ld(), bmc_covert::satisfying_assignment(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), path_strategy_choosert::set_path_strategy_options(), cbmc_parse_optionst::set_properties(), jbmc_parse_optionst::set_properties(), janalyzer_parse_optionst::set_properties(), goto_analyzer_parse_optionst::set_properties(), propt::set_time_limit_seconds(), bmct::setup(), java_bytecode_convert_methodt::setup_local_variables(), show_class_hierarchy(), show_goto_functions(), show_properties(), interpretert::show_state(), language_uit::show_symbol_table(), language_uit::show_symbol_table_xml_ui(), bmct::show_vcc(), java_bytecode_parsert::skip_bytes(), skip_loops(), bmct::slice(), smt2_parsert::sort(), splice_call(), static_simplifier(), static_verifier(), fault_localizationt::stop_on_fail(), bmct::stop_on_fail(), string_identifiers_resolution_from_equations(), goto_symext::symex_assign_symbol(), goto_symext::symex_goto(), 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(), 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(), 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(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), c_typecheck_baset::typecheck_while(), smt2_parsert::unary(), shared_bufferst::unique(), jsil_typecheckt::update_expr_type(), 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(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 302 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(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), string_constraint_generatort::add_axioms_for_format_specifier(), cpp_typecheckt::add_base_components(), compilet::add_files_from_archive(), linker_script_merget::add_linker_script_definitions(), compilet::add_written_cprover_symbols(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), bv_refinementt::arrays_overapproximated(), as_modet::as_hybrid_binary(), gcc_modet::asm_output(), languaget::build_stub_parameter_symbol(), 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(), arrayst::collect_arrays(), cpp_declarator_convertert::combine_types(), cpp_declarator_convertert::convert(), 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_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(), 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(), goto_convertt::convert_return(), boolbvt::convert_struct(), 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(), boolbvt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), smt2_dect::dec_solve(), string_refinementt::dec_solve(), c_typecheck_baset::designator_enter(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_template_classes(), 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(), bmct::do_language_agnostic_bmc(), 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(), clobber_parse_optionst::doit(), jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), compilet::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), typecheckt::err_location(), smt2_tokenizert::error(), error_parse_line(), interpretert::evaluate(), interpretert::evaluate_address(), bmct::execute(), interpretert::execute_assert(), interpretert::execute_assign(), interpretert::execute_function_call(), interpretert::execute_other(), language_uit::final(), lazy_goto_modelt::finalize(), goto_convertt::finish_gotos(), cpp_typecheckt::full_member_initialization(), gcc_modet::gcc_hybrid_binary(), generate_ansi_c_start_function(), generate_java_start_function(), 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(), jbmc_parse_optionst::get_command_line_options(), cpp_typecheckt::get_component(), get_cover_config(), cbmc_parse_optionst::get_goto_program(), jbmc_parse_optionst::get_goto_program(), get_main_symbol(), bmct::get_memory_model(), get_module(), get_module_by_name(), cbmc_solverst::get_smt2(), goto_convertt::get_string_constant(), interpretert::get_value(), linker_script_merget::goto_and_object_mismatch(), goto_convert(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_declarator_convertert::handle_initializer(), hybrid_binary(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), lazy_goto_modelt::initialize(), initialize_goto_model(), cpp_typecheckt::instantiate_template(), instrument_cover_goals(), goto_instrument_parse_optionst::instrument_goto_program(), java_bytecode_parse(), jsil_entry_point(), satcheck_minisat2_baset< Minisat::Solver >::lcnf(), satcheck_glucose_baset< Glucose::SimpSolver >::lcnf(), ld_modet::ld_hybrid_binary(), linkingt::link_error(), 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(), 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()(), bmc_all_propertiest::operator()(), cover_goalst::operator()(), prop_minimizet::operator()(), taint_analysist::operator()(), interpretert::operator()(), goto_difft::output_functions(), 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(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), linker_script_merget::pointerize_linker_defined_symbols(), linker_script_merget::pointerize_subexprs_of(), java_bytecode_parsert::pool_entry(), java_bytecode_convert_methodt::pop(), cbmc_parse_optionst::preprocessing(), jbmc_parse_optionst::process_goto_function(), jbmc_parse_optionst::process_goto_functions(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_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_glucose_baset< Glucose::SimpSolver >::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(), read_goto_binary(), java_class_loadert::read_jar_file(), smt2_dect::read_result(), arrayst::record_array_equality(), 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(), linker_script_merget::replace_expr(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), path_strategy_choosert::set_path_strategy_options(), satcheck_minisat2_baset< Minisat::Solver >::set_polarity(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), cbmc_parse_optionst::set_properties(), jbmc_parse_optionst::set_properties(), janalyzer_parse_optionst::set_properties(), goto_analyzer_parse_optionst::set_properties(), language_uit::show_symbol_table(), language_uit::show_symbol_table_xml_ui(), bmct::show_vcc(), java_bytecode_parsert::skip_bytes(), skip_loops(), splice_call(), 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(), 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(), 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(), 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(), and cpp_typecheckt::zero_initializer().
|
static |
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
user_input | Input string; if empty, the default verbosity is used. |
default_verbosity | Verbosity to use if no value is provided. |
dest | message handler the verbosity of which is to be set. |
Definition at line 78 of file message.cpp.
References M_DEBUG, M_WARNING, message_handlert::print(), message_handlert::set_verbosity(), to_string(), and unsafe_string2unsigned().
Referenced by as_modet::doit(), armcc_modet::doit(), cw_modet::doit(), ms_cl_modet::doit(), ld_modet::doit(), gcc_modet::doit(), clobber_parse_optionst::doit(), jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), and goto_analyzer_parse_optionst::doit().
|
inline |
Definition at line 153 of file message.h.
References INVARIANT, and message_handler.
Referenced by linker_script_merget::add_linker_script_definitions(), bmct::all_properties(), cpp_typecheckt::builtin_factory(), java_bytecode_convert_methodt::convert_invoke_dynamic(), java_bytecode_languaget::convert_lazy_method(), java_bytecode_languaget::convert_single_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(), bmct::do_language_agnostic_bmc(), goto_instrument_parse_optionst::do_remove_const_function_pointers_only(), jdiff_parse_optionst::doit(), clobber_parse_optionst::doit(), goto_diff_parse_optionst::doit(), compilet::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), ci_lazy_methodst::entry_point_methods(), bmct::execute(), fault_localizationt::fault_localizationt(), java_bytecode_convert_methodt::find_initializers_for_slot(), gcc_modet::gcc_hybrid_binary(), jbmc_parse_optionst::generate_function_body(), ansi_c_languaget::generate_support_functions(), cpp_languaget::generate_support_functions(), jsil_languaget::generate_support_functions(), java_bytecode_languaget::generate_support_functions(), cbmc_solverst::get_bv_refinement(), java_class_loadert::get_class_from_jar(), cbmc_solverst::get_default(), cbmc_solverst::get_dimacs(), goto_instrument_parse_optionst::get_goto_program(), jbmc_parse_optionst::get_goto_program(), java_bytecode_languaget::get_language_options(), linker_script_merget::get_linker_script_data(), java_class_loadert::get_parse_tree(), cbmc_solverst::get_smt2(), cbmc_solverst::get_string_refinement(), initialize_goto_model(), goto_instrument_parse_optionst::instrument_goto_program(), jsil_languaget::interfaces(), ld_modet::ld_hybrid_binary(), compilet::link(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), bv_minimizing_dect::minimize(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), bv_minimizet::operator()(), taint_analysist::operator()(), java_class_loadert::operator()(), bmc_covert::operator()(), java_bytecode_convert_classt::operator()(), ansi_c_languaget::parse(), cpp_parsert::parse(), jsil_languaget::parse(), cpp_languaget::parse(), language_uit::parse(), compilet::parse(), java_bytecode_languaget::parse(), compilet::parse_stdin(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), ansi_c_languaget::preprocess(), cpp_languaget::preprocess(), cbmc_parse_optionst::preprocessing(), jbmc_parse_optionst::process_goto_function(), jbmc_parse_optionst::process_goto_functions(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), remove_function_pointerst::remove_function_pointer(), fault_localizationt::run_decision_procedure(), bmct::run_decision_procedure(), java_class_loader_limitt::setup_class_load_limit(), jbmc_parse_optionst::show_loaded_functions(), java_bytecode_instrumentt::throw_exception(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), ansi_c_languaget::typecheck(), cpp_languaget::typecheck(), jsil_languaget::typecheck(), java_bytecode_languaget::typecheck(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_type(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 296 of file message.h.
References messaget::mstreamt::message_level, and mstream.
Referenced by debug(), error(), progress(), result(), statistics(), status(), and warning().
Definition at line 175 of file message.h.
References messaget::mstreamt::assign_from(), message_handler, and mstream.
|
inline |
Definition at line 327 of file message.h.
References get_mstream(), and M_PROGRESS.
Referenced by bv_refinementt::arrays_overapproximated(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), bv_refinementt::dec_solve(), goto_inlinet::expand_function_call(), goto_inlinet::goto_inline_transitive(), static_simplifier(), and static_verifier().
|
inline |
Definition at line 312 of file message.h.
References get_mstream(), and M_RESULT.
Referenced by linkingt::adjust_object_type(), linkingt::adjust_object_type_rec(), arith_left_shift(), arith_right_shift(), as_modet::as_hybrid_binary(), property_checkert::as_string(), gcc_modet::asm_output(), binary2integer(), bitwise_and(), bitwise_neg(), bitwise_or(), bitwise_xor(), string_abstractiont::build(), string_abstractiont::build_unknown(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_unbounded_array(), interpretert::byte_offset_to_memory_offset(), smt2_parsert::cast_bv_to_signed(), bv_refinementt::check_SAT(), java_class_loadert::class_name_to_file(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), interpretert::command(), interpretert::concretize_type(), prop_conv_solvert::convert(), java_bytecode_convert_methodt::convert(), ci_lazy_methodst::convert_and_analyze_method(), prop_conv_solvert::convert_bool(), boolbvt::convert_bswap(), 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_group_json(), goto_difft::convert_function_json(), smt2_convt::convert_identifier(), boolbvt::convert_index(), 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(), interpretert::count_type_leaves(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_instrument_parse_optionst::doit(), equalityt::equality2(), bmct::error_trace(), interpretert::evaluate(), interpretert::evaluate_address(), qbf_bdd_certificatet::f_get(), java_class_loadert::file_to_class_name(), smt2_parsert::function_application(), cpp_typecheckt::function_identifier(), ci_lazy_methodst::gather_virtual_callsites(), 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(), interpretert::get_value(), cnf_clause_listt::hash(), qdimacs_cnft::hash(), cnf_clause_listt::hash_clause(), java_bytecode_instrumentt::instrument_expr(), goto_instrument_parse_optionst::instrument_goto_program(), integer2binary(), integer2string(), satcheck_booleforce_baset::l_get(), satcheck_lingelingt::l_get(), satcheck_picosatt::l_get(), satcheck_zchaff_baset::l_get(), satcheck_minisat1_baset::l_get(), ld_modet::ld_hybrid_binary(), smt2_parsert::let_expression(), prop_conv_solvert::literal(), logic_left_shift(), logic_right_shift(), c_typecheck_baset::make_already_typechecked(), goto_convertt::make_compound_literal(), string_abstractiont::member(), interpretert::memory_offset_to_byte_offset(), smt2_parsert::multi_ary(), propt::new_variables(), smt2_parsert::operands(), smt2irept::operator()(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), goto_difft::output_function(), goto_difft::output_function_group(), goto_difft::output_functions(), bmct::output_graphml(), smt2irept::parse(), ansi_c_languaget::parse(), cpp_languaget::parse(), jsil_languaget::parse(), smt2_convt::parse_struct(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), linker_script_merget::pointerize_subexprs_of(), qbf_qubet::prop_solve(), qbf_quantort::prop_solve(), qbf_skizzot::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_booleforce_baset::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_squolem_coret::prop_solve(), qbf_squolemt::prop_solve(), pbs_dimacs_cnft::prop_solve(), bv_refinementt::prop_solve(), smt2_parsert::quantifier_expression(), java_bytecode_parsert::read_bytes(), bmc_all_propertiest::report(), clobber_parse_optionst::report_failure(), bmct::report_failure(), clobber_parse_optionst::report_success(), bmct::report_success(), rotate_left(), rotate_right(), prop_conv_solvert::set_equality_to_true(), java_bytecode_convert_methodt::setup_local_variables(), show_class_hierarchy(), show_properties(), show_properties_json(), 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(), java_bytecode_convert_methodt::try_catch_handler(), type2name(), type2name_symbol(), 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(), and java_bytecode_convert_methodt::variable().
|
inlinevirtual |
Reimplemented in aig_prop_solvert.
Definition at line 148 of file message.h.
References message_handler.
Referenced by add_library(), bmct::all_properties(), mmcc_parse_optionst::convert(), convert(), bmct::cover(), bmct::decide(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), fault_localizationt::fault_localizationt(), language_uit::final(), generate_ansi_c_start_function(), cbmc_solverst::get_bv_refinement(), lazy_goto_modelt::initialize(), initialize_goto_model(), java_bytecode_parse(), jsil_entry_point(), language_uit::language_uit(), load_java_class(), bv_minimizing_dect::minimize(), model_argc_argv(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), bv_minimizet::operator()(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(), bmc_covert::operator()(), ansi_c_languaget::parse(), jsil_languaget::parse(), cpp_languaget::parse(), cpp_parsert::parse(), language_uit::parse(), compilet::parse(), java_bytecode_languaget::parse(), parse_json(), compilet::parse_stdin(), parse_xml(), cbmc_parse_optionst::preprocessing(), fault_localizationt::run_decision_procedure(), bmct::run_decision_procedure(), aig_prop_solvert::set_message_handler(), solver(), to_expr(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), and language_uit::typecheck().
|
inline |
Definition at line 322 of file message.h.
References get_mstream(), and M_STATISTICS.
Referenced by partial_order_concurrencyt::build_event_lists(), aig_prop_solvert::compute_phase(), prop_conv_solvert::dec_solve(), compilet::doit(), bmct::execute(), symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), instrumentert::goto2graph_cfg(), instrumentert::instrument_minimum_interference_inserter(), compilet::link(), memory_model_tsot::operator()(), memory_model_psot::operator()(), memory_model_sct::operator()(), bmc_covert::operator()(), compilet::parse(), compilet::parse_stdin(), read_object_and_link(), remove_function_pointerst::remove_function_pointer(), remove_unused_functions(), bmct::slice(), symex_bmct::symex_step(), aig_prop_solvert::usage_count(), and compilet::write_bin_object_file().
|
inline |
Definition at line 317 of file message.h.
References get_mstream(), and M_STATUS.
Referenced by interpretert::assign(), instrumentert::cfg_cycles_filter(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), interpretert::command(), compilet::compile(), qbf_bdd_coret::compress_certificate(), satcheck_zchaff_baset::copy_cnf(), event_grapht::copy_segment(), bv_refinementt::dec_solve(), bmct::do_conversion(), goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(), bmct::do_language_agnostic_bmc(), 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(), jdiff_parse_optionst::doit(), clobber_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), bmct::error_trace(), java_bytecode_convert_methodt::find_initializers_for_slot(), 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(), cbmc_parse_optionst::get_goto_program(), jbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), get_module(), instrumentert::goto2graph_cfg(), lazy_goto_modelt::initialize(), initialize_goto_model(), instrument_cover_goals(), goto_instrument_parse_optionst::instrument_goto_program(), satcheck_booleforce_baset::l_get(), satcheck_zchaff_baset::l_get(), counterexample_beautificationt::operator()(), bmc_all_propertiest::operator()(), prop_minimizet::operator()(), taint_analysist::operator()(), interpretert::operator()(), bmc_covert::operator()(), language_uit::parse(), java_bytecode_languaget::parse(), pbs_dimacs_cnft::pbs_solve(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), jbmc_parse_optionst::process_goto_functions(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), qbf_quantort::prop_solve(), qbf_skizzot::prop_solve(), qbf_qubet::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_booleforce_baset::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_picosatt::prop_solve(), satcheck_zchaff_baset::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_minisat1_baset::prop_solve(), qbf_squolem_coret::prop_solve(), qbf_squolemt::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::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(), fault_localizationt::run(), fault_localizationt::run_decision_procedure(), bmct::run_decision_procedure(), satcheck_zchaff_baset::satcheck_zchaff_baset(), bmc_covert::satisfying_assignment(), satcheck_glucose_simplifiert::set_frozen(), satcheck_minisat_simplifiert::set_frozen(), bmct::setup(), show_goto_functions(), interpretert::show_state(), static_simplifier(), static_verifier(), fault_localizationt::stop_on_fail(), language_uit::typecheck(), java_bytecode_languaget::typecheck(), language_filest::typecheck_module(), and weak_memory().
|
inline |
Definition at line 307 of file message.h.
References get_mstream(), and M_WARNING.
Referenced by string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_format_specifier(), compilet::add_input_file(), shared_bufferst::assignment(), string_abstractiont::build_wrap(), event_grapht::graph_pensieve_explorert::collect_pairs(), compilet::compile(), interpretert::concretize_type(), java_bytecode_convert_classt::convert(), goto_convertt::convert_gcc_switch_case_range(), create_stub_global_symbols(), cpp_typecheck_resolvet::do_builtin(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_list(), as_modet::doit(), ms_cl_modet::doit(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), error_parse_line(), interpretert::evaluate(), goto_inlinet::expand_function_call(), compilet::find_library(), generate_class_stub(), generate_function_bodies(), generate_function_bodies_factory(), linker_script_merget::get_linker_script_data(), java_class_loadert::get_parse_tree(), java_string_library_preprocesst::get_primitive_value_of_object(), havoc_generate_function_bodiest::havoc_expr_rec(), prop_conv_solvert::ignoring(), c_typecheck_baset::implicit_typecast(), linkingt::link_warning(), member_type_lazy(), model_argc_argv(), symex_bmct::no_body(), shared_bufferst::nondet_flush(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), populate_predecessor_map(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), remove_function(), remove_function_pointerst::remove_function_pointer(), goto_inlinet::replace_return(), cover_basic_blockst::report_block_anomalies(), propt::set_time_limit_seconds(), java_bytecode_convert_methodt::setup_local_variables(), java_bytecode_languaget::typecheck(), 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().
|
protected |
Definition at line 342 of file message.h.
Referenced by conditional_output(), eom(), language_uit::final(), get_message_handler(), goto_instrument_parse_optionst::instrument_goto_program(), messaget::mstreamt::json_stream(), messaget::mstreamt::operator<<(), operator=(), set_message_handler(), java_bytecode_languaget::to_expr(), language_uit::typecheck(), and typecheckt::typecheck_main().
|
mutableprotected |
Definition at line 343 of file message.h.
Referenced by conditional_output(), get_mstream(), operator=(), and remove_function_pointerst::remove_function_pointer().