cprover
messaget::mstreamt Class Reference

#include <message.h>

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

Public Member Functions

 mstreamt (unsigned _message_level, messaget &_message)
 
 mstreamt (const mstreamt &other)=delete
 
 mstreamt (const mstreamt &other, messaget &_message)
 
mstreamtoperator= (const mstreamt &other)=delete
 
mstreamtoperator<< (const xmlt &data)
 
mstreamtoperator<< (const json_objectt &data)
 
template<class T >
mstreamtoperator<< (const T &x)
 
mstreamtoperator<< (mstreamt &(*func)(mstreamt &))
 
json_stream_arraytjson_stream ()
 Returns a reference to the top-level JSON array stream. More...
 

Public Attributes

unsigned message_level
 
messagetmessage
 
source_locationt source_location
 

Private Member Functions

void assign_from (const mstreamt &other)
 

Friends

class messaget
 

Detailed Description

Definition at line 190 of file message.h.

Constructor & Destructor Documentation

◆ mstreamt() [1/3]

messaget::mstreamt::mstreamt ( unsigned  _message_level,
messaget _message 
)
inline

Definition at line 193 of file message.h.

◆ mstreamt() [2/3]

messaget::mstreamt::mstreamt ( const mstreamt other)
delete

◆ mstreamt() [3/3]

messaget::mstreamt::mstreamt ( const mstreamt other,
messaget _message 
)
inline

Definition at line 203 of file message.h.

Member Function Documentation

◆ assign_from()

void messaget::mstreamt::assign_from ( const mstreamt other)
inlineprivate

Definition at line 260 of file message.h.

References message_level, and source_location.

Referenced by messaget::operator=().

◆ json_stream()

json_stream_arrayt& messaget::mstreamt::json_stream ( )
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().

◆ operator<<() [1/4]

mstreamt& messaget::mstreamt::operator<< ( const xmlt data)
inline

◆ operator<<() [2/4]

mstreamt& messaget::mstreamt::operator<< ( const json_objectt data)
inline

◆ operator<<() [3/4]

template<class T >
mstreamt& messaget::mstreamt::operator<< ( const T &  x)
inline

Definition at line 239 of file message.h.

◆ operator<<() [4/4]

mstreamt& messaget::mstreamt::operator<< ( mstreamt &(*)(mstreamt &)  func)
inline

Definition at line 246 of file message.h.

◆ operator=()

mstreamt& messaget::mstreamt::operator= ( const mstreamt other)
delete

Friends And Related Function Documentation

◆ messaget

friend class messaget
friend

Definition at line 267 of file message.h.

Member Data Documentation

◆ message

◆ message_level

unsigned messaget::mstreamt::message_level

◆ source_location

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().


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