cprover
|
#include <message.h>
Public Member Functions | |
mstreamt (unsigned _message_level, messaget &_message) | |
mstreamt (const mstreamt &other)=delete | |
mstreamt (const mstreamt &other, messaget &_message) | |
mstreamt & | operator= (const mstreamt &other)=delete |
mstreamt & | operator<< (const xmlt &data) |
mstreamt & | operator<< (const json_objectt &data) |
template<class T > | |
mstreamt & | operator<< (const T &x) |
mstreamt & | operator<< (mstreamt &(*func)(mstreamt &)) |
json_stream_arrayt & | json_stream () |
Returns a reference to the top-level JSON array stream. More... | |
Public Attributes | |
unsigned | message_level |
messaget & | message |
source_locationt | source_location |
Private Member Functions | |
void | assign_from (const mstreamt &other) |
Friends | |
class | messaget |
|
inline |
|
delete |
|
inlineprivate |
Definition at line 260 of file message.h.
References message_level, and source_location.
Referenced by messaget::operator=().
|
inline |
Returns a reference to the top-level JSON array stream.
Definition at line 252 of file message.h.
References messaget::eom(), message_handlert::get_json_stream(), message, and messaget::message_handler.
Referenced by bmct::error_trace(), bmc_covert::operator()(), bmc_all_propertiest::report(), and show_class_hierarchy().
Definition at line 216 of file message.h.
References messaget::eom(), message, messaget::message_handler, message_level, and message_handlert::print().
|
inline |
Definition at line 227 of file message.h.
References messaget::eom(), message, messaget::message_handler, message_level, and message_handlert::print().
|
inline |
messaget& messaget::mstreamt::message |
Definition at line 213 of file message.h.
Referenced by event_grapht::graph_explorert::backtrack(), instrumentert::cfg_visitort::contains_shared_array(), messaget::eom(), json_stream(), operator<<(), instrumentert::cfg_visitort::visit_cfg_duplicate(), and instrumentert::cfg_visitort::visit_cfg_reference_function().
unsigned messaget::mstreamt::message_level |
Definition at line 212 of file message.h.
Referenced by assign_from(), messaget::conditional_output(), messaget::eom(), messaget::get_mstream(), and operator<<().
source_locationt messaget::mstreamt::source_location |
Definition at line 214 of file message.h.
Referenced by cpp_typecheckt::add_anonymous_members_to_scope(), c_typecheck_baset::add_argc_argv(), cpp_typecheckt::add_base_components(), c_typecheck_baset::apply_asm_label(), assign_from(), cpp_typecheckt::check_member_initializers(), cpp_typecheckt::class_template_symbol(), goto_convertt::clean_expr(), cpp_declarator_convertert::combine_types(), instrumentert::cfg_visitort::contains_shared_array(), cpp_declarator_convertert::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(), 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(), 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(), 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_list(), goto_convertt::do_input(), goto_convertt::do_output(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), messaget::eom(), typecheckt::err_location(), smt2_tokenizert::error(), error_parse_line(), bmct::execute(), goto_inlinet::expand_function_call(), goto_convertt::finish_gotos(), cpp_typecheckt::full_member_initialization(), goto_convertt::get_array_argument(), cpp_typecheckt::get_component(), goto_convertt::get_string_constant(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_declarator_convertert::handle_initializer(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), lazy_goto_modelt::initialize(), initialize_goto_model(), cpp_typecheckt::instantiate_template(), linkingt::link_error(), linkingt::link_warning(), cpp_declarator_convertert::main_function_rules(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), cpp_typecheckt::move_member_initializers(), c_typecheck_baset::move_symbol(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), language_uit::parse(), parsert::parse_error(), linker_script_merget::pointerize_linker_defined_symbols(), cpp_typecheckt::put_compound_into_scope(), cpp_typecheckt::reference_initializer(), goto_convertt::remove_assignment(), 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(), goto_inlinet::replace_return(), fault_localizationt::report(), cover_basic_blockst::report_block_anomalies(), fault_localizationt::report_xml(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), show_properties(), goto_symext::symex_goto(), Parser::SyntaxError(), cpp_typecheckt::template_suffix(), c_typecheck_baset::typecheck_array_type(), 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(), 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_custom_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), cpp_typecheckt::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_throw(), cpp_typecheckt::typecheck_expr_trinary(), 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(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_return(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_symbol(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typedef_type(), c_typecheck_baset::typecheck_vector_type(), ansi_c_convert_typet::write(), and cpp_typecheckt::zero_initializer().