cprover
|
#include <stdexcept>
#include <type_traits>
#include <string>
#include <cstdlib>
Go to the source code of this file.
Classes | |
class | invariant_failedt |
A logic error, augmented with a distinguished field to hold a backtrace. More... | |
Macros | |
#define | __this_function__ __func__ |
#define | INVARIANT(CONDITION, REASON) |
#define | INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) |
#define | PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") |
#define | PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
#define | POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") |
#define | POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
#define | CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") |
#define | CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
#define | UNREACHABLE INVARIANT(false, "Unreachable") |
#define | UNREACHABLE_STRUCTURED(TYPENAME, ...) INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) |
#define | DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) |
#define | DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
#define | TODO INVARIANT(false, "Todo") |
#define | UNIMPLEMENTED INVARIANT(false, "Unimplemented") |
#define | UNHANDLED_CASE INVARIANT(false, "Unhandled case") |
Functions | |
void | print_backtrace (std::ostream &out) |
Prints a back trace to 'out'. More... | |
std::string | get_backtrace () |
Returns a backtrace. More... | |
void | report_exception_to_stderr (const invariant_failedt &) |
Dump exception report to stderr. More... | |
template<class ET , typename ... Params> | |
std::enable_if< std::is_base_of< invariant_failedt, ET >::value >::type | invariant_violated_structured (const std::string &file, const std::string &function, const int line, Params &&... params) |
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace). More... | |
void | invariant_violated_string (const std::string &file, const std::string &function, const int line, const std::string &reason) |
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant's description. More... | |
#define __this_function__ __func__ |
Definition at line 202 of file invariant.h.
#define CHECK_RETURN | ( | CONDITION | ) | INVARIANT(CONDITION, "Check return value") |
Definition at line 245 of file invariant.h.
Referenced by string_constraint_generatort::add_axioms_for_char_literal(), string_constraint_generatort::add_axioms_from_int_with_radix(), trace_automatont::add_dtrans(), add_generic_type_information(), add_node(), interpretert::address_to_object_record(), endianness_mapt::build_big_endian(), c_nondet_symbol_factory(), bv_refinementt::check_SAT(), bv_pointerst::convert_address_of_rec(), boolbvt::convert_bitwise(), boolbvt::convert_bswap(), boolbvt::convert_byte_extract(), goto_difft::convert_function_json(), dump_ct::convert_global_variable(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), smt2_convt::convert_plus(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), cpp_exception_id(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::do_virtual_table(), interpretert::evaluate(), smt2_parsert::expression(), get_current_working_directory(), get_data_type(), get_fresh_aux_symbol(), get_length_type(), select_pointer_typet::get_recursively_instantiated_type(), interpretert::get_size(), ci_lazy_methodst::handle_virtual_methods_with_no_callees(), dump_ct::insert_local_static_decls(), dump_ct::insert_local_type_decls(), is_not_zero(), exprt::is_one(), is_store_to_slot(), exprt::is_zero(), json(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), lower_popcount(), map_bv(), object_factory(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), dump_ct::operator()(), goto_difft::output_function(), pbs_dimacs_cnft::pbs_solve(), pointer_offset_bits_as_string(), qbf_quantort::prop_solve(), qbf_skizzot::prop_solve(), qbf_qubet::prop_solve(), qbf_qube_coret::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), remove_function_pointerst::remove_function_pointer(), str2number(), temp_working_dirt::temp_working_dirt(), sparse_arrayt::to_if_expression(), interval_sparse_arrayt::to_if_expression(), type2name(), type_checked_cast(), cpp_typecheckt::typecheck_compound_declarator(), java_bytecode_convert_methodt::variable(), cpp_typecheckt::zero_initializer(), and temp_working_dirt::~temp_working_dirt().
#define CHECK_RETURN_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 246 of file invariant.h.
#define DATA_INVARIANT | ( | CONDITION, | |
REASON | |||
) | INVARIANT(CONDITION, REASON) |
Definition at line 257 of file invariant.h.
Referenced by arrayst::add_array_constraints(), arrayst::add_array_constraints_array_of(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), string_constraint_generatort::add_axioms_for_function_application(), add_padding_gcc(), add_to_json(), add_to_xml(), cpp_typecheck_resolvet::apply_template_args(), bv_refinementt::arrays_overapproximated(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), template_mapt::build(), build_sizeof_expr(), c_preprocess_visual_studio(), check_and_replace_target(), arrayst::collect_arrays(), compute_pointer_offset(), goto_programt::compute_target_numbers(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), goto_convertt::convert_assign(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitwise(), boolbvt::convert_case(), dump_ct::convert_compound(), boolbvt::convert_cond(), java_bytecode_convert_methodt::convert_const(), convert_decl(), boolbvt::convert_equality(), smt2_convt::convert_expr(), boolbvt::convert_floatbv_op(), java_bytecode_convert_methodt::convert_instructions(), boolbvt::convert_overflow(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), java_bytecode_convert_methodt::convert_switch(), boolbvt::convert_verilog_case_equality(), cpp_typecheckt::cpp_is_pod(), string_refinementt::dec_solve(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer(), interpretert::evaluate(), interpretert::execute_other(), smt2_solvert::expand_function_applications(), expr_initializert< nondet >::expr_initializer_rec(), flatten_byte_extract(), namespace_baset::follow(), remove_exceptionst::function_or_callees_may_throw(), goto_programt::get_decl_identifiers(), goto_programt::get_end_function(), java_bytecode_languaget::get_language_options(), java_string_library_preprocesst::get_primitive_value_of_object(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), goto_inline(), goto_inlinet::goto_inline(), goto_inlinet::goto_inline_transitive(), goto_inlinet::insert_function_body(), remove_exceptionst::instrument_function_call(), custom_bitvector_domaint::is_bottom(), escape_domaint::is_bottom(), global_may_alias_domaint::is_bottom(), uninitialized_domaint::is_bottom(), interval_domaint::is_bottom(), is_threaded_domaint::is_bottom(), dep_graph_domaint::is_bottom(), rd_range_domaint::is_bottom(), uninitialized_domaint::is_top(), custom_bitvector_domaint::is_top(), escape_domaint::is_top(), global_may_alias_domaint::is_top(), dep_graph_domaint::is_top(), rd_range_domaint::is_top(), json(), dep_graph_domaint::make_bottom(), dep_graph_domaint::make_entry(), dep_graph_domaint::make_top(), member_offset_expr(), model_argc_argv(), goto_symex_statet::level0t::operator()(), member_offset_iterator::operator++(), constant_propagator_domaint::valuest::output(), goto_programt::output_instruction(), cmdlinet::parse(), arrayst::record_array_equality(), goto_symex_statet::rename(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rmethod(), configt::set_object_bits_from_symbol_table(), simplify_exprt::simplify_extractbits(), size_of_expr(), stack_depth(), substitute_array_lists(), goto_symext::symex_goto(), goto_symext::symex_other(), to_abs_expr(), to_address_of_expr(), to_array_of_expr(), to_binary_expr(), to_binary_relation_expr(), to_bswap_expr(), to_complex_expr(), to_dereference_expr(), to_div_expr(), to_dynamic_object_expr(), to_equal_expr(), to_extractbit_expr(), to_extractbits_expr(), to_factorial_expr(), to_factorial_power_expr(), to_floatbv_typecast_expr(), to_function_application_expr(), to_ieee_float_equal_expr(), to_ieee_float_notequal_expr(), to_ieee_float_op_expr(), to_if_expr(), to_implies_expr(), to_index_designator(), to_index_expr(), to_isfinite_expr(), to_isinf_expr(), to_isnan_expr(), to_isnormal_expr(), to_let_expr(), to_member_designator(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_nondet_symbol_expr(), to_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_plus_expr(), to_popcount_expr(), to_power_expr(), to_quantifier_expr(), to_rem_expr(), to_replication_expr(), to_shift_expr(), to_string_not_contains_constraint(), to_symbol_expr(), to_trans_expr(), to_typecast_expr(), to_unary_expr(), to_unary_minus_expr(), to_union_expr(), to_update_expr(), to_with_expr(), uncaught_exceptions_domaint::transform(), cpp_typecheckt::typecheck_decl(), java_bytecode_typecheckt::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), undefined_function_abort_path(), update_index_set(), validate_expr(), validate_operands(), and validate_type().
#define DATA_INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 258 of file invariant.h.
#define INVARIANT | ( | CONDITION, | |
REASON | |||
) |
Definition at line 205 of file invariant.h.
Referenced by arrayst::add_array_constraints(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_format_specifier(), string_constraint_generatort::add_axioms_for_index_of(), trace_automatont::add_dstate(), add_generic_type_information(), full_slicert::add_jumps(), event_grapht::add_node(), goto_symext::address_arithmetic(), address_bits(), allocate_dynamic_object(), bv_refinementt::arrays_overapproximated(), cover_basic_blockst::block_of(), cover_basic_blocks_javat::block_of(), bmct::bmct(), build_graph(), disjunctive_polynomial_accelerationt::build_path(), check_and_replace_target(), bv_refinementt::check_SAT(), irept::compare(), compute_inverse_function(), goto_programt::compute_location_numbers(), dep_graph_domaint::control_dependencies(), java_bytecode_convert_methodt::convert(), prop_conv_solvert::convert_bool(), convert_decl(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), goto_convertt::convert_label(), cpp_typecheckt::convert_parameter(), select_pointer_typet::convert_pointer_type(), java_bytecode_languaget::convert_single_method(), small_mapt< innert >::copy_and_erase(), small_mapt< innert >::copy_and_insert(), copy_on_writet< T >::copy_on_writet(), cover_basic_blockst::cover_basic_blockst(), create_clinit_wrapper_symbols(), create_static_function_call(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbol(), create_stub_global_symbols(), copy_on_write_pointeet< Num >::decrement_use_count(), trace_automatont::determinise(), dirtyt::die_if_uninitialized(), java_bytecode_convert_methodt::do_exception_handling(), remove_returnst::do_function_calls(), bmct::do_language_agnostic_bmc(), data_dpt::dp_merge(), symbol_tablet::erase(), string_transformation_builtin_functiont::eval(), find_closing_delimiter(), find_closing_semi_colon_for_reference_type(), java_bytecode_convert_methodt::find_initializers_for_slot(), reachability_slicert::fixedpoint_from_assertions(), reachability_slicert::fixedpoint_to_assertions(), string_dependenciest::for_each_dependency(), format_specifier_of_match(), ci_lazy_methods_neededt::gather_field_types(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_pointer_target_init(), generate_constant_global_variables(), string_refinementt::get(), path_strategy_choosert::get(), get_clinit_wrapper_body(), jbmc_parse_optionst::get_command_line_options(), get_current_working_directory(), unified_difft::get_diff(), remove_virtual_functionst::get_functions(), remove_exceptionst::get_inflight_exception_global(), get_language_from_identifier(), get_ldc_result(), get_main_symbol(), messaget::get_message_handler(), base_ref_infot::get_name_and_type(), get_or_create_class_literal_symbol(), get_or_create_string_literal_symbol(), select_pointer_typet::get_recursively_instantiated_type(), method_handle_infot::get_reference(), java_bytecode_convert_methodt::get_static_field(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), symex_bmct::get_unwind(), symex_bmct::get_unwind_recursion(), ci_lazy_methodst::get_virtual_method_targets(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), havoc_generate_function_bodiest::havoc_expr_rec(), copy_on_write_pointeet< Num >::increment_use_count(), infer_opaque_type_fields(), goto_symext::initialize_entry_point(), array_poolt::insert(), goto_unwindt::unwind_logt::insert(), recursion_set_entryt::insert_entry(), generic_parameter_specialization_map_keyst::insert_pairs(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), instantiate(), cover_basic_blockst::instruction_of(), cover_mcdc_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), remove_exceptionst::instrument_exceptions(), interval_sparse_arrayt::interval_sparse_arrayt(), is_store_to_slot(), java_array_element_type(), java_bytecode_instrument_symbol(), java_enum_static_init_unwind_handler(), java_generic_symbol_typet::java_generic_symbol_typet(), java_generic_type_from_string(), java_local_variable_slots(), java_type_from_string(), join_types(), ui_message_handlert::json_ui_msg(), satcheck_glucose_baset< Glucose::SimpSolver >::lcnf(), satcheck_minisat2_baset< Minisat::Solver >::lcnf(), link_functions(), load_java_class(), long_double_type(), remove_instanceoft::lower_instanceof(), java_string_library_preprocesst::make_float_to_string_code(), java_string_library_preprocesst::make_init_from_array_code(), java_string_library_preprocesst::make_string_format_code(), member_type_lazy(), value_set_dereferencet::memory_model_bytes(), is_threaded_domaint::merge(), constant_propagator_domaint::valuest::merge(), java_bytecode_languaget::methods_provided(), depth_iteratort::mutate(), irept::nonrecursive_destructor(), template_numberingt< exprt >::number(), union_find< exprt >::number(), numeric_cast_v(), remove_returnst::operator()(), unified_difft::operator()(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(), procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned >::operator()(), java_qualifierst::operator=(), sparse_vectort< memory_cellt >::operator[](), irept::ordering(), constant_propagator_domaint::valuest::output(), parse_list_types(), java_bytecode_parsert::parse_local_variable_type_table(), bmct::perform_symbolic_execution(), pointer_diff_type(), populate_predecessor_map(), populate_variable_address_map(), gcc_modet::preprocess(), ui_message_handlert::print(), event_grapht::critical_cyclet::print_name(), cnft::process_clause(), jbmc_parse_optionst::process_goto_function(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rclass_attribute(), structured_pool_entryt::read_utf8_constant(), goto_program2codet::remove_const(), remove_virtual_functionst::remove_virtual_function(), remove_returnst::replace_returns(), sparse_vectort< memory_cellt >::resize(), java_bytecode_parsert::rmethod_attribute(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assumptions(), set_class_identifier(), string_refinementt::set_to(), constant_propagator_domaint::valuest::set_to_top(), size_type(), slice_global_inits(), small_mapt< innert >::small_mapt(), cover_basic_blockst::source_location_of(), split_string(), static_show_domain(), static_unreachable_instructions(), static_verifier(), string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(), string_containert::string_containert(), substitute_array_access(), goto_symext::symex_allocate(), goto_symext::symex_goto(), grapht< abstract_eventt >::topsort(), constant_propagator_domaint::transform(), is_threaded_domaint::transform(), cpp_typecheckt::typecheck_compound_declarator(), java_bytecode_typecheckt::typecheck_expr(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_type(), ui_message_handlert::ui_message_handlert(), remove_returnst::undo_function_calls(), cover_basic_blockst::update_covered_lines(), arrayst::update_index_map(), cpp_typecheckt::user_defined_conversion_sequence(), utf16_constant_array_to_java(), validate_expr(), copy_on_writet< T >::write(), and ui_message_handlert::~ui_message_handlert().
#define INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) |
Definition at line 213 of file invariant.h.
Referenced by cpp_typecheckt::class_template_symbol(), reaching_definitions_analysist::get_state(), goto_symex_statet::l2_thread_read_encoding(), invariant_sett::output(), rd_range_domaint::transform(), rd_range_domaint::transform_assign(), and cpp_typecheckt::typecheck_template_args().
#define POSTCONDITION | ( | CONDITION | ) | INVARIANT(CONDITION, "Postcondition") |
Definition at line 237 of file invariant.h.
Referenced by dump_ct::cleanup_decl(), dump_ct::cleanup_type(), dump_ct::convert_compound(), irept::detach(), bv_pointerst::do_postponed(), dump_ct::dump_typedefs(), prop_minimizet::fix_objectives(), Parser::merge_types(), model_argc_argv(), and java_bytecode_parsert::read_bootstrapmethods_entry().
#define POSTCONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 238 of file invariant.h.
#define PRECONDITION | ( | CONDITION | ) | INVARIANT(CONDITION, "Precondition") |
Definition at line 230 of file invariant.h.
Referenced by actuals_replace_map(), bv_refinementt::add_approximation(), string_constraint_generatort::add_axioms_for_char_at(), string_constraint_generatort::add_axioms_for_char_literal(), string_constraint_generatort::add_axioms_for_char_set(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_code_point_at(), string_constraint_generatort::add_axioms_for_code_point_before(), string_constraint_generatort::add_axioms_for_code_point_count(), string_constraint_generatort::add_axioms_for_compare_to(), string_constraint_generatort::add_axioms_for_concat(), string_constraint_generatort::add_axioms_for_concat_char(), string_constraint_generatort::add_axioms_for_concat_code_point(), string_constraint_generatort::add_axioms_for_constrain_characters(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_delete_char_at(), string_constraint_generatort::add_axioms_for_empty_string(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_hash_code(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_insert_bool(), string_constraint_generatort::add_axioms_for_insert_char(), string_constraint_generatort::add_axioms_for_insert_double(), string_constraint_generatort::add_axioms_for_insert_int(), string_constraint_generatort::add_axioms_for_intern(), string_constraint_generatort::add_axioms_for_is_empty(), string_constraint_generatort::add_axioms_for_is_prefix(), string_constraint_generatort::add_axioms_for_is_suffix(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_length(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_replace(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_char(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), string_constraint_generatort::add_axioms_from_int(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_int_with_radix(), string_constraint_generatort::add_axioms_from_literal(), string_constraint_generatort::add_axioms_from_long(), add_character_set_constraint(), string_constraint_generatort::add_constraint_on_characters(), add_dependency_to_string_subexprs(), add_generic_type_information(), add_pointer_to_array_association(), goto_inlinet::goto_inline_logt::add_segment(), add_to_json(), add_to_xml(), automatont::add_trans(), goto_symext::address_arithmetic(), advance_to_next_key(), arith_left_shift(), arith_right_shift(), disjunctive_polynomial_accelerationt::assert_for_values(), symex_target_equationt::assignment(), goto_symex_statet::assignment(), string_constraint_generatort::associate_array_to_pointer(), string_constraint_generatort::associate_length_to_array(), string_exprt< array_string_exprt >::axiom_for_has_length(), string_exprt< array_string_exprt >::axiom_for_length_ge(), string_exprt< array_string_exprt >::axiom_for_length_gt(), string_exprt< array_string_exprt >::axiom_for_length_le(), string_exprt< array_string_exprt >::axiom_for_length_lt(), interpretert::base_address_to_alloc_size(), base_ref_infot::base_ref_infot(), bitwise_and(), bitwise_neg(), bitwise_or(), bitwise_xor(), dirtyt::build(), build_class_name(), disjunctive_polynomial_accelerationt::build_fixed(), resolve_inherited_componentt::build_full_component_identifier(), disjunctive_polynomial_accelerationt::build_path(), bv_refinementt::bv_refinementt(), goto_symex_statet::call_stack(), goto_inlinet::check_inline_map(), bv_refinementt::check_UNSAT(), class_infot::class_infot(), dump_ct::cleanup_expr(), java_string_library_preprocesst::code_assign_components_to_java_string(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), dump_ct::collect_typedefs_rec(), goto_programt::instructiont::complete_goto(), prop_conv_solvert::convert_bool(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), character_refine_preprocesst::convert_digit_char(), bv_refinementt::convert_div(), java_string_library_preprocesst::convert_exprt_to_string_exprt(), java_bytecode_convert_methodt::convert_instructions(), language_filest::convert_lazy_method(), bv_refinementt::convert_mod(), bv_refinementt::convert_mult(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), bv_cbmct::convert_waitfor_symbol(), small_mapt< innert >::copy_and_erase(), small_mapt< innert >::copy_and_insert(), goto_inlinet::goto_inline_logt::copy_from(), compilet::cprover_macro_arities(), cpp_token_buffert::current_token(), symex_target_equationt::decl(), small_shared_two_way_pointeet< Num >::decrement_use_count(), depth_iteratort::depth_iteratort(), goto_symext::dereference(), dereference_exprt::dereference_exprt(), bv_pointerst::do_postponed(), dump_ct::dump_typedefs(), small_mapt< innert >::erase(), string_concat_char_builtin_functiont::eval(), string_insertion_builtin_functiont::eval(), interpretert::execute_decl(), interpretert::execute_function_call(), goto_inlinet::expand_function_call(), expr_checked_cast(), java_bytecode_languaget::final(), small_mapt< innert >::find(), find_closing_delimiter(), find_closing_semi_colon_for_reference_type(), floatbv_mult(), call_grapht::format_callsites(), from_integer(), gather_full_class_name(), dump_ct::gather_global_typedefs(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_pointer_target_init(), generate_ansi_c_start_function(), generate_function_bodiest::generate_function_body(), java_bytecode_languaget::generate_support_functions(), get_all_generic_parameters(), goto_inlinet::get_call(), get_common_dominator(), refined_string_typet::get_content_type(), get_data_type(), get_default_language(), small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >::get_derived_u(), small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >::get_derived_v(), goto_programt::get_end_function(), uncaught_exceptions_domaint::get_exception_type(), small_mapt< innert >::get_field(), format_elementt::get_format_specifier(), format_elementt::get_format_text(), goto_programt::get_function_id(), get_function_name(), refined_string_typet::get_index_type(), ui_message_handlert::get_json_stream(), get_length_type(), invariant_sett::get_object(), get_or_create_string_literal_symbol(), cpp_idt::get_parent(), java_class_loadert::get_parse_tree(), java_bytecode_languaget::get_pointer_type_selector(), rw_range_sett::get_ranges(), rw_guarded_range_set_value_sett::get_ranges(), get_significand(), symex_target_equationt::get_SSA_step(), get_string_argument_rec(), string_constraint_generatort::get_string_expr(), goto_programt::instructiont::get_target(), get_thread_block_identifier(), interpretert::get_value(), ci_lazy_methodst::get_virtual_method_targets(), goto_inlinet::goto_inline(), goto_inlinet::goto_inline_nontransitive(), goto_inlinet::goto_inline_transitive(), goto_symex_statet::renaming_levelt::increase_counter(), small_shared_two_way_pointeet< Num >::increment_use_count(), initial_index_set(), goto_symext::initialize_entry_point(), initialize_nondet_string_struct(), goto_programt::insert_before_swap(), goto_inlinet::insert_function_body(), dump_ct::insert_local_static_decls(), generic_parameter_specialization_map_keyst::insert_pairs(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), cover_basic_blocks_javat::instruction_of(), instrument_endThread(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), instrument_getCurrentThreadID(), goto_instrument_parse_optionst::instrument_goto_program(), instrument_start_thread(), remove_exceptionst::instrument_throw(), integer2size_t(), integer2ulong(), integer2unsigned(), interval_sparse_arrayt::interval_sparse_arrayt(), is_digit_with_radix(), satcheck_glucose_simplifiert::is_eliminated(), satcheck_minisat_simplifiert::is_eliminated(), java_add_components_to_class(), java_generic_class_type_bound(), java_generic_class_type_var(), java_generic_get_inst_type(), java_generic_symbol_typet::java_generic_symbol_typet(), java_generic_type_from_string(), java_type_from_string(), length_constraint_for_concat_substr(), lift_if(), load_java_class(), logic_left_shift(), logic_right_shift(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), java_string_library_preprocesst::make_assign_and_return_function_from_call(), make_binary(), array_poolt::make_char_array_for_char_pointer(), make_clean_pointer_cast(), java_string_library_preprocesst::make_float_to_string_code(), boolbvt::make_free_bv_expr(), java_string_library_preprocesst::make_init_from_array_code(), java_string_library_preprocesst::make_init_function_from_call(), java_string_library_preprocesst::make_string_format_code(), make_with_expr(), map_bv(), maybe_add_hole(), constant_propagator_domaint::valuest::merge(), symex_bmct::merge_goto(), method_handle_infot::method_handle_infot(), automatont::move(), depth_iterator_baset< const_depth_iteratort >::mutate(), name_and_type_infot::name_and_type_infot(), goto_convertt::new_tmp_symbol(), depth_iterator_baset< const_depth_iteratort >::next_sibling_or_parent(), not_exprt::not_exprt(), operator &=(), dump_ct::operator()(), resolve_inherited_componentt::operator()(), java_bytecode_convert_classt::operator()(), numeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type >::operator()(), local_may_alias_factoryt::operator()(), depth_iterator_baset< const_depth_iteratort >::operator*(), depth_iterator_baset< const_depth_iteratort >::operator++(), small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >::operator=(), small_mapt< innert >::operator[](), operator|=(), goto_inlinet::output_inline_map(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), java_bytecode_languaget::parse(), parse_list_types(), path_storaget::peek(), path_storaget::pop(), goto_symext::pop_frame(), power(), path_lifot::private_pop(), java_string_library_preprocesst::process_equals_function_operands(), satcheck_glucose_baset< Glucose::SimpSolver >::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), json_stream_arrayt::push_back(), json_stream_arrayt::push_back_stream_array(), json_stream_objectt::push_back_stream_array(), json_stream_arrayt::push_back_stream_object(), json_stream_objectt::push_back_stream_object(), remove_calls_no_bodyt::remove_call_no_body(), irept::remove_ref(), goto_symex_statet::rename_address(), require_goto_statements::require_struct_array_component_assignment(), resolve_inherited_componentt::resolve_inherited_componentt(), goto_symex_statet::level1t::restore_from(), goto_symext::return_assignment(), goto_symext::rewrite_quantifiers(), rotate_left(), rotate_right(), run(), gcc_modet::run_gcc(), ld_modet::run_ld(), satcheck_minisat2_baset< Minisat::Solver >::set_assignment(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assignment(), set_class_identifier(), small_mapt< innert >::set_field(), satcheck_glucose_baset< Glucose::SimpSolver >::set_polarity(), satcheck_minisat2_baset< Minisat::Solver >::set_polarity(), boolbvt::set_to(), string_refinementt::set_to(), prop_conv_solvert::set_to(), small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >::small_shared_two_way_ptrt(), cover_basic_blocks_javat::source_location_of(), sparse_arrayt::sparse_arrayt(), split_string(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), string_insertion_builtin_functiont::string_insertion_builtin_functiont(), string_transformation_builtin_functiont::string_transformation_builtin_functiont(), strip_java_namespace_prefix(), sum_overflows(), small_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >::swap(), goto_symex_statet::switch_to_thread(), goto_symext::symex_allocate(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), goto_symext::symex_step(), goto_symext::symex_with_state(), to_abs_expr(), to_address_of_expr(), to_and_expr(), to_array_expr(), to_array_of_expr(), to_array_string_expr(), to_array_type(), to_bitand_expr(), to_bitnot_expr(), to_bitor_expr(), to_bitvector_type(), to_bitxor_expr(), to_bswap_expr(), to_bv_type(), to_c_bit_field_type(), to_c_bool_type(), to_c_enum_tag_type(), to_c_enum_type(), to_class_type(), to_code_type(), to_complex_expr(), to_complex_type(), to_concatenation_expr(), to_constant_expr(), to_cpp_name(), to_cpp_template_args_non_tc(), to_cpp_template_args_tc(), to_dereference_expr(), to_div_expr(), to_dynamic_object_expr(), to_enumeration_type(), to_equal_expr(), to_extractbit_expr(), to_extractbits_expr(), to_factorial_expr(), to_factorial_power_expr(), to_fixedbv_type(), to_floatbv_type(), to_floatbv_typecast_expr(), to_function_application_expr(), to_ieee_float_equal_expr(), to_ieee_float_notequal_expr(), to_if_expr(), to_implies_expr(), to_incomplete_array_type(), to_index_designator(), to_index_expr(), to_isfinite_expr(), to_isinf_expr(), to_isnan_expr(), to_isnormal_expr(), to_java_generic_class_type(), to_java_generic_parameter(), to_java_generic_symbol_type(), to_java_generic_type(), to_java_implicitly_generic_class_type(), to_let_expr(), to_mathematical_function_type(), to_member_designator(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_nondet_symbol_expr(), to_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_or_expr(), to_plus_expr(), to_pointer_type(), to_popcount_expr(), to_power_expr(), to_range_type(), to_reference_type(), to_refined_string_type(), to_rem_expr(), to_replication_expr(), to_signedbv_type(), invariant_sett::to_string(), to_string_expr(), to_string_not_contains_constraint(), to_string_type(), to_struct_expr(), to_struct_tag_type(), to_struct_type(), to_struct_union_type(), to_symbol_expr(), to_symbol_type(), to_tag_type(), to_template_type(), to_trans_expr(), to_typecast_expr(), to_unary_minus_expr(), to_union_expr(), to_union_tag_type(), to_union_type(), to_unsignedbv_type(), to_update_expr(), to_vector_expr(), to_vector_type(), to_with_expr(), to_xor_expr(), goto_symex_statet::top(), java_generic_parametert::type_variable(), java_generic_parametert::type_variable_ref(), java_bytecode_languaget::typecheck(), c_typecheck_baset::typecheck_array_type(), java_bytecode_typecheckt::typecheck_expr_java_new(), java_bytecode_typecheckt::typecheck_expr_java_new_array(), java_bytecode_typecheckt::typecheck_expr_symbol(), typecheckt::typecheck_main(), c_typecheck_baset::typecheck_redefinition_non_type(), smt2_convt::use_array_theory(), utf16_constant_array_to_java(), validate(), validate_expr(), and generic_parameter_specialization_map_keyst::~generic_parameter_specialization_map_keyst().
#define PRECONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 231 of file invariant.h.
#define TODO INVARIANT(false, "Todo") |
Definition at line 265 of file invariant.h.
Referenced by bv_refinementt::check_SAT().
#define UNHANDLED_CASE INVARIANT(false, "Unhandled case") |
Definition at line 267 of file invariant.h.
#define UNIMPLEMENTED INVARIANT(false, "Unimplemented") |
Definition at line 266 of file invariant.h.
Referenced by string_constraint_generatort::add_axioms_for_char_literal(), string_insertion_builtin_functiont::add_constraints(), boolbvt::convert_bitwise(), string_insertion_builtin_functiont::length_constraint(), string_builtin_function_with_no_evalt::length_constraint(), and show_class_hierarchy().
#define UNREACHABLE INVARIANT(false, "Unreachable") |
Definition at line 250 of file invariant.h.
Referenced by string_abstractiont::abstract(), bv_refinementt::add_approximation(), cpp_typecheckt::add_base_components(), string_insertion_builtin_functiont::add_constraints(), string_concatenation_builtin_functiont::add_constraints(), compilet::add_input_file(), c_typecheck_baset::add_rounding_mode(), java_object_factoryt::allocate_object(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), cpp_typecheck_resolvet::apply_template_args(), assert_l1_renaming(), assert_l2_renaming(), simplify_exprt::bits2expr(), ansi_c_declaratort::build(), string_abstractiont::build(), build_graph_rec(), goto_program2codet::build_loop_map(), build_ssa_identifier_rec(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), byte_extract_id(), byte_update_id(), bv_refinementt::check_SAT(), partial_order_concurrencyt::clock(), symex_slicet::collect_open_variables(), monomialt::compare(), complex_member(), struct_union_typet::component_number(), goto_program_coverage_recordt::compute_coverage_lines(), cfg_baset< cfg_nodet >::compute_edges(), constant_float(), cpp_declarator_convertert::convert(), bv_pointerst::convert_address_of_rec(), symex_target_equationt::convert_assertions(), boolbvt::convert_byte_update(), goto_program2codet::convert_catch(), dump_ct::convert_compound(), expr2javat::convert_constant(), goto_convertt::convert_cpp_delete(), smt2_convt::convert_div(), convert_float_literal(), goto_program2codet::convert_goto_switch(), cpp_typecheckt::convert_initializer(), goto_program2codet::convert_instruction(), smt2_convt::convert_minus(), smt2_convt::convert_mult(), smt2_convt::convert_overflow(), smt2_convt::convert_plus(), goto_program2codet::convert_throw(), cpp_typecheckt::cpp_constructor(), goto_convertt::cpp_new_initializer(), goto_symext::dereference_rec(), c_typecheck_baset::designator_enter(), ieee_floatt::divide_and_round(), c_typecheck_baset::do_designated_initializer(), bmct::do_language_agnostic_bmc(), cpp_typecheckt::do_not_typechecked(), bv_pointerst::do_postponed(), goto_convertt::do_printf(), goto_convertt::do_scanf(), cpp_typecheckt::dynamic_typecast(), cpp_typecheck_resolvet::filter(), flatten_byte_extract(), bv_spect::from_type(), ansi_c_declarationt::full_type(), generate_ansi_c_start_function(), string_refinementt::get(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), get_inherited_component(), message_handlert::get_json_stream(), goto_cc_cmdlinet::get_optnr(), java_string_library_preprocesst::get_primitive_value_of_object(), expr2ct::get_shorthands(), bv_refinementt::get_values(), goto_rw(), c_typecastt::implicit_typecast_arithmetic(), invariant_sett::implies_rec(), value_set_fivrt::object_map_dt::insert(), value_set_fivrnst::object_map_dt::insert(), prop_convt::is_in_conflict(), java_array_type(), java_type_from_char(), string_insertion_builtin_functiont::length_constraint(), string_concatenation_builtin_functiont::length_constraint(), timestampert::make(), value_set_fit::make_union(), make_with_expr(), max_value(), model_argc_argv(), bv_utilst::multiplier(), bv_utilst::multiplier_no_overflow(), goto_checkt::nan_check(), operator &=(), operator<<(), operator|=(), Parser::optCvQualify(), Parser::optMemberSpec(), Parser::optStorageSpec(), goto_trace_stept::output(), symex_target_equationt::SSA_stept::output(), change_impactt::output_change_impact(), goto_programt::output_instruction(), bv_utilst::overflow_add(), bv_utilst::overflow_sub(), java_bytecode_languaget::parse(), Parser::rBaseSpecifiers(), Parser::rClassMember(), Parser::rClassSpec(), read_bin_goto_object_v3(), cpp_convert_typet::read_function_type(), ansi_c_convert_typet::read_rec(), bv_utilst::rel(), goto_convertt::remove_assignment(), sharing_node_innert< key_type, mapped_type >::remove_leaf(), clobber_parse_optionst::report_failure(), clobber_parse_optionst::report_success(), Parser::rTemplateDecl(), Parser::rTypePredicate(), Parser::rUnaryExpr(), partial_order_concurrencyt::rw_clock_id(), template_mapt::set(), configt::ansi_ct::set_arch_spec_alpha(), configt::ansi_ct::set_arch_spec_arm(), configt::ansi_ct::set_arch_spec_hppa(), configt::ansi_ct::set_arch_spec_i386(), configt::ansi_ct::set_arch_spec_ia64(), configt::ansi_ct::set_arch_spec_mips(), configt::ansi_ct::set_arch_spec_power(), configt::ansi_ct::set_arch_spec_s390(), configt::ansi_ct::set_arch_spec_s390x(), configt::ansi_ct::set_arch_spec_sh4(), configt::ansi_ct::set_arch_spec_sparc(), configt::ansi_ct::set_arch_spec_x32(), configt::ansi_ct::set_arch_spec_x86_64(), prop_convt::set_assumptions(), goto_program2codet::set_block_end_points(), prop_convt::set_frozen(), goto_symex_statet::set_ssa_indices(), bv_utilst::shift(), clobber_parse_optionst::show_counterexample(), show_goto_trace(), show_locations(), show_loop_ids(), show_properties(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_not_constant(), symex_slicet::slice(), bmc_all_propertiest::goalt::status_string(), invariant_sett::strengthen_rec(), goto_symext::symex_assign_byte_extract(), goto_symext::symex_other(), goto_symext::symex_start_thread(), custom_bitvector_domaint::transform(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_compound_body(), c_typecheck_baset::typecheck_compound_type(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), cpp_typecheckt::typecheck_expr_typecast(), c_typecheck_baset::typecheck_side_effect_statement_expression(), goto_unwindt::unwind(), unwrap_exception(), and ansi_c_convert_typet::write().
#define UNREACHABLE_STRUCTURED | ( | TYPENAME, | |
... | |||
) | INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) |
Definition at line 251 of file invariant.h.
std::string get_backtrace | ( | ) |
Returns a backtrace.
Definition at line 104 of file invariant.cpp.
References print_backtrace().
Referenced by invariant_violated_structured().
|
inline |
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant's description.
In future this may throw rather than aborting.
file | : C string giving the name of the file. |
function | : C string giving the name of the function. |
line | : The line number of the invariant |
reason | : brief description of the invariant violation. |
Definition at line 183 of file invariant.h.
std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type invariant_violated_structured | ( | const std::string & | file, |
const std::string & | function, | ||
const int | line, | ||
Params &&... | params | ||
) |
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace).
In future this may throw reason
instead of aborting. Template parameter ET: type of exception to construct
file | : C string giving the name of the file. |
function | : C string giving the name of the function. |
line | : The line number of the invariant |
params | : (variadic) parameters to forward to ET's constructor its backtrace member will be set before it is used. |
Definition at line 159 of file invariant.h.
References get_backtrace(), and report_exception_to_stderr().
void print_backtrace | ( | std::ostream & | out | ) |
Prints a back trace to 'out'.
out | Stream to print backtrace |
Definition at line 78 of file invariant.cpp.
References stack.
Referenced by get_backtrace().
void report_exception_to_stderr | ( | const invariant_failedt & | ) |
Dump exception report to stderr.
Definition at line 112 of file invariant.cpp.
Referenced by invariant_violated_structured().