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(0, "Todo") |
#define | UNIMPLEMENTED INVARIANT(0, "Unimplemented") |
#define | UNHANDLED_CASE INVARIANT(0, "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 199 of file invariant.h.
#define CHECK_RETURN | ( | CONDITION | ) | INVARIANT(CONDITION, "Check return value") |
Definition at line 240 of file invariant.h.
Referenced by dump_ct::convert_global_variable(), 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(), dump_ct::operator()(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), remove_function_pointerst::remove_function_pointer(), and java_bytecode_convert_methodt::variable().
#define CHECK_RETURN_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 241 of file invariant.h.
#define DATA_INVARIANT | ( | CONDITION, | |
REASON | |||
) | INVARIANT(CONDITION, REASON) |
Definition at line 252 of file invariant.h.
Referenced by dump_ct::convert_compound(), java_bytecode_convert_methodt::convert_instructions(), exprt::negate(), to_abs_expr(), to_address_of_expr(), to_array_of_expr(), to_binary_expr(), to_binary_relation_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_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_plus_expr(), to_power_expr(), to_rem_expr(), to_replication_expr(), to_shift_expr(), to_symbol_expr(), to_trans_expr(), to_typecast_expr(), to_unary_expr(), to_unary_minus_expr(), to_union_expr(), to_update_expr(), and to_with_expr().
#define DATA_INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 253 of file invariant.h.
#define INVARIANT | ( | CONDITION, | |
REASON | |||
) |
Definition at line 202 of file invariant.h.
Referenced by irept::compare(), java_bytecode_convert_methodt::convert_instructions(), java_object_factoryt::gen_nondet_struct_init(), messaget::get_message_handler(), value_set_dereferencet::memory_model_bytes(), irept::nonrecursive_destructor(), irept::ordering(), gcc_modet::preprocess(), grapht< abstract_eventt >::topsort(), and cpp_typecheckt::user_defined_conversion_sequence().
#define INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) |
Definition at line 209 of file invariant.h.
Referenced by cpp_typecheckt::class_template_symbol(), path_symex_step_reft::generate_successor(), path_symex_step_reft::get(), path_symex_step_reft::get_history(), reaching_definitions_analysist::get_state(), cpp_typecheckt::instantiate_template(), path_symex_statet::is_symbol_member_index(), goto_symex_statet::l2_thread_read_encoding(), goto_symex_statet::l2_thread_write_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 232 of file invariant.h.
Referenced by dump_ct::cleanup_decl(), dump_ct::cleanup_type(), dump_ct::convert_compound(), irept::detach(), and dump_ct::dump_typedefs().
#define POSTCONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 233 of file invariant.h.
#define PRECONDITION | ( | CONDITION | ) | INVARIANT(CONDITION, "Precondition") |
Definition at line 225 of file invariant.h.
Referenced by dump_ct::cleanup_expr(), dump_ct::collect_typedefs_rec(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), java_bytecode_convert_methodt::convert_instructions(), dump_ct::dump_typedefs(), dump_ct::gather_global_typedefs(), invariant_sett::get_object(), cpp_idt::get_parent(), rw_range_sett::get_ranges(), rw_guarded_range_set_value_sett::get_ranges(), dump_ct::insert_local_static_decls(), lift_if(), make_binary(), make_with_expr(), dump_ct::operator()(), local_may_alias_factoryt::operator()(), path_symex_statet::pc(), irept::remove_ref(), gcc_modet::run_gcc(), to_abs_expr(), to_address_of_expr(), to_and_expr(), to_array_expr(), to_array_of_expr(), to_bitand_expr(), to_bitnot_expr(), to_bitor_expr(), to_bitxor_expr(), to_complex_expr(), to_concatenation_expr(), to_constant_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_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_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_or_expr(), to_plus_expr(), to_power_expr(), to_rem_expr(), to_replication_expr(), invariant_sett::to_string(), to_struct_expr(), to_symbol_expr(), to_trans_expr(), to_typecast_expr(), to_unary_minus_expr(), to_union_expr(), to_update_expr(), to_vector_expr(), to_with_expr(), and c_typecheck_baset::typecheck_array_type().
#define PRECONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) |
Definition at line 226 of file invariant.h.
#define TODO INVARIANT(0, "Todo") |
Definition at line 260 of file invariant.h.
#define UNHANDLED_CASE INVARIANT(0, "Unhandled case") |
Definition at line 262 of file invariant.h.
#define UNIMPLEMENTED INVARIANT(0, "Unimplemented") |
Definition at line 261 of file invariant.h.
#define UNREACHABLE INVARIANT(false, "Unreachable") |
Definition at line 245 of file invariant.h.
Referenced by dump_ct::convert_compound(), smt2_convt::convert_div(), smt2_convt::convert_minus(), smt2_convt::convert_mult(), smt2_convt::convert_overflow(), smt2_convt::convert_plus(), gcc_modet::doit(), make_with_expr(), and exprt::negate().
#define UNREACHABLE_STRUCTURED | ( | TYPENAME, | |
... | |||
) | INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) |
Definition at line 246 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_failedt::invariant_failedt(), and 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 180 of file invariant.h.
References invariant_failedt::file, invariant_failedt::line, and invariant_failedt::reason.
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.
ET | : (template type parameter), 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 156 of file invariant.h.
References invariant_failedt::backtrace, 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 77 of file invariant.cpp.
Referenced by get_backtrace(), and invariant_failedt::invariant_failedt().
void report_exception_to_stderr | ( | const invariant_failedt & | ) |
Dump exception report to stderr.
Definition at line 112 of file invariant.cpp.
Referenced by invariant_failedt::invariant_failedt(), and invariant_violated_structured().