cprover
invariant.h File Reference
#include <stdexcept>
#include <type_traits>
#include <string>
#include <cstdlib>
Include dependency graph for invariant.h:
This graph shows which files directly or indirectly include this file:

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

Macro Definition Documentation

◆ __this_function__

#define __this_function__   __func__

Definition at line 199 of file invariant.h.

◆ CHECK_RETURN

◆ CHECK_RETURN_STRUCTURED

#define CHECK_RETURN_STRUCTURED (   CONDITION,
  TYPENAME,
  ... 
)    INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

Definition at line 241 of file invariant.h.

◆ DATA_INVARIANT

◆ DATA_INVARIANT_STRUCTURED

#define DATA_INVARIANT_STRUCTURED (   CONDITION,
  TYPENAME,
  ... 
)    INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

Definition at line 253 of file invariant.h.

◆ INVARIANT

◆ INVARIANT_STRUCTURED

◆ POSTCONDITION

#define POSTCONDITION (   CONDITION)    INVARIANT(CONDITION, "Postcondition")

◆ POSTCONDITION_STRUCTURED

#define POSTCONDITION_STRUCTURED (   CONDITION,
  TYPENAME,
  ... 
)    INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

Definition at line 233 of file invariant.h.

◆ PRECONDITION

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

◆ PRECONDITION_STRUCTURED

#define PRECONDITION_STRUCTURED (   CONDITION,
  TYPENAME,
  ... 
)    INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

Definition at line 226 of file invariant.h.

◆ TODO

#define TODO   INVARIANT(0, "Todo")

Definition at line 260 of file invariant.h.

◆ UNHANDLED_CASE

#define UNHANDLED_CASE   INVARIANT(0, "Unhandled case")

Definition at line 262 of file invariant.h.

◆ UNIMPLEMENTED

#define UNIMPLEMENTED   INVARIANT(0, "Unimplemented")

Definition at line 261 of file invariant.h.

◆ UNREACHABLE

◆ UNREACHABLE_STRUCTURED

#define UNREACHABLE_STRUCTURED (   TYPENAME,
  ... 
)    INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)

Definition at line 246 of file invariant.h.

Function Documentation

◆ get_backtrace()

std::string get_backtrace ( )

Returns a backtrace.

Returns
backtrace with a file / function / line header.

Definition at line 104 of file invariant.cpp.

References print_backtrace().

Referenced by invariant_violated_structured().

◆ invariant_violated_string()

void invariant_violated_string ( const std::string &  file,
const std::string &  function,
const int  line,
const std::string &  reason 
)
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.

Parameters
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.

◆ invariant_violated_structured()

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

In future this may throw reason instead of aborting.

Parameters
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 get_backtrace(), and report_exception_to_stderr().

◆ print_backtrace()

void print_backtrace ( std::ostream &  out)

Prints a back trace to 'out'.

Parameters
outStream to print backtrace

Definition at line 77 of file invariant.cpp.

References free(), and stack.

Referenced by get_backtrace().

◆ report_exception_to_stderr()

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