cprover
invariant.h File Reference
#include <cstdlib>
#include <sstream>
#include <stdexcept>
#include <string>
#include <type_traits>
+ Include dependency graph for invariant.h:

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...
 
class  invariant_with_diagnostics_failedt
 A class that includes diagnostic information related to an invariant violation. More...
 
struct  detail::always_falset< T >
 
struct  diagnostics_helpert< T >
 Helper to give us some diagnostic in a usable form on assertion failure. More...
 
struct  diagnostics_helpert< char[N]>
 
struct  diagnostics_helpert< char * >
 
struct  diagnostics_helpert< std::string >
 

Namespaces

 detail
 

Macros

#define CBMC_NORETURN
 
#define EXPAND_MACRO(x)   x
 
#define CURRENT_FUNCTION_NAME   __func__
 
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)
 
#define INVARIANT(CONDITION, REASON)
 This macro uses the wrapper function 'invariant_violated_string'. More...
 
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...)
 Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'. More...
 
#define PRECONDITION(CONDITION)   INVARIANT(CONDITION, "Precondition")
 
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...)   INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)
 
#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...)   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
#define POSTCONDITION(CONDITION)   INVARIANT(CONDITION, "Postcondition")
 
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...)   INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)
 
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...)   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
#define CHECK_RETURN(CONDITION)   INVARIANT(CONDITION, "Check return value")
 
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...)   INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)
 
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...)   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
#define UNREACHABLE   INVARIANT(false, "Unreachable")
 This should be used to mark dead code. More...
 
#define UNREACHABLE_STRUCTURED(TYPENAME, ...)   EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
 
#define DATA_INVARIANT(CONDITION, REASON)   INVARIANT(CONDITION, REASON)
 This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc. More...
 
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...)   INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
 
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)   EXPAND_MACRO(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, const std::string &condition, Params &&... params)
 This function is the backbone of all the invariant types. More...
 
void invariant_violated_string (const std::string &file, const std::string &function, const int line, const std::string &condition, const std::string &reason)
 This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'. More...
 
std::string detail::assemble_diagnostics ()
 
template<typename T >
std::string detail::diagnostic_as_string (T &&val)
 
void detail::write_rest_diagnostics (std::ostream &)
 
template<typename T , typename... Ts>
void detail::write_rest_diagnostics (std::ostream &out, T &&next, Ts &&... rest)
 
template<typename... Diagnostics>
std::string detail::assemble_diagnostics (Diagnostics &&... args)
 
template<typename... Diagnostics>
void report_invariant_failure (const std::string &file, const std::string &function, int line, std::string reason, std::string condition, Diagnostics &&... diagnostics)
 This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'. More...
 

Macro Definition Documentation

◆ CBMC_NORETURN

#define CBMC_NORETURN

Definition at line 157 of file invariant.h.

◆ CHECK_RETURN

#define CHECK_RETURN (   CONDITION)    INVARIANT(CONDITION, "Check return value")

Definition at line 470 of file invariant.h.

◆ CHECK_RETURN_STRUCTURED

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

Definition at line 474 of file invariant.h.

◆ CHECK_RETURN_WITH_DIAGNOSTICS

#define CHECK_RETURN_WITH_DIAGNOSTICS (   CONDITION,
  ... 
)    INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)

Definition at line 471 of file invariant.h.

◆ CURRENT_FUNCTION_NAME

#define CURRENT_FUNCTION_NAME   __func__

Definition at line 379 of file invariant.h.

◆ DATA_INVARIANT

#define DATA_INVARIANT (   CONDITION,
  REASON 
)    INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.

being well formed. "The data structure is not corrupt or malformed"

Definition at line 485 of file invariant.h.

◆ DATA_INVARIANT_STRUCTURED

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

Definition at line 489 of file invariant.h.

◆ DATA_INVARIANT_WITH_DIAGNOSTICS

#define DATA_INVARIANT_WITH_DIAGNOSTICS (   CONDITION,
  REASON,
  ... 
)    INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)

Definition at line 486 of file invariant.h.

◆ EXPAND_MACRO

#define EXPAND_MACRO (   x)    x

Definition at line 371 of file invariant.h.

◆ INVARIANT

#define INVARIANT (   CONDITION,
  REASON 
)
Value:
do \
{ \
if(!(CONDITION)) \
{ \
invariant_violated_string( \
__FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON); \
} \
} while(false)
#define CURRENT_FUNCTION_NAME
Definition: invariant.h:379

This macro uses the wrapper function 'invariant_violated_string'.

Definition at line 398 of file invariant.h.

◆ INVARIANT_STRUCTURED

#define INVARIANT_STRUCTURED (   CONDITION,
  TYPENAME,
  ... 
)
Value:
do /* NOLINT */ \
{ \
if(!(CONDITION)) \
invariant_violated_structured<TYPENAME>( \
__FILE__, \
CURRENT_FUNCTION_NAME, \
__LINE__, \
#CONDITION, \
__VA_ARGS__); /* NOLINT */ \
} while(false)

Definition at line 382 of file invariant.h.

◆ INVARIANT_WITH_DIAGNOSTICS

#define INVARIANT_WITH_DIAGNOSTICS (   CONDITION,
  REASON,
  ... 
)
Value:
do \
{ \
if(!(CONDITION)) \
{ \
report_invariant_failure( \
__FILE__, \
__LINE__, \
REASON, \
__VA_ARGS__); \
} \
} while(false)
#define CURRENT_FUNCTION_NAME
Definition: invariant.h:379

Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'.

Definition at line 412 of file invariant.h.

◆ POSTCONDITION

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

Definition at line 454 of file invariant.h.

◆ POSTCONDITION_STRUCTURED

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

Definition at line 458 of file invariant.h.

◆ POSTCONDITION_WITH_DIAGNOSTICS

#define POSTCONDITION_WITH_DIAGNOSTICS (   CONDITION,
  ... 
)    INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)

Definition at line 455 of file invariant.h.

◆ PRECONDITION

#define PRECONDITION (   CONDITION)    INVARIANT(CONDITION, "Precondition")

Definition at line 438 of file invariant.h.

◆ PRECONDITION_STRUCTURED

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

Definition at line 442 of file invariant.h.

◆ PRECONDITION_WITH_DIAGNOSTICS

#define PRECONDITION_WITH_DIAGNOSTICS (   CONDITION,
  ... 
)    INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)

Definition at line 439 of file invariant.h.

◆ TODO

#define TODO   INVARIANT(false, "Todo")

Definition at line 496 of file invariant.h.

◆ UNHANDLED_CASE

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

Definition at line 498 of file invariant.h.

◆ UNIMPLEMENTED

#define UNIMPLEMENTED   INVARIANT(false, "Unimplemented")

Definition at line 497 of file invariant.h.

◆ UNREACHABLE

#define UNREACHABLE   INVARIANT(false, "Unreachable")

This should be used to mark dead code.

Definition at line 478 of file invariant.h.

◆ UNREACHABLE_STRUCTURED

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

Definition at line 479 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 102 of file invariant.cpp.

◆ invariant_violated_string()

void invariant_violated_string ( const std::string &  file,
const std::string &  function,
const int  line,
const std::string &  condition,
const std::string &  reason 
)
inline

This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.

It constructs an invariant_violatedt from reason and the backtrace, then aborts after printing the invariant's description. In future this may throw rather than aborting.

Parameters
fileC string giving the name of the file.
functionC string giving the name of the function.
lineThe line number of the invariant
reasonbrief description of the invariant violation.
conditionthe condition this invariant is checking.

Definition at line 250 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,
const std::string &  condition,
Params &&...  params 
)

This function is the backbone of all the invariant types.

Every instance of an invariant is ultimately generated by this function template, which is at times called via a wrapper function. 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

Parameters
fileC string giving the name of the file.
functionC string giving the name of the function.
lineThe line number of the invariant
conditionthe condition this invariant is checking.
params(variadic) parameters to forward to ET's constructor its backtrace member will be set before it is used.

Definition at line 218 of file invariant.h.

◆ print_backtrace()

void print_backtrace ( std::ostream &  out)

Prints a back trace to 'out'.

Parameters
outStream to print backtrace

Definition at line 78 of file invariant.cpp.

◆ report_exception_to_stderr()

void report_exception_to_stderr ( const invariant_failedt )

Dump exception report to stderr.

Definition at line 110 of file invariant.cpp.

◆ report_invariant_failure()

template<typename... Diagnostics>
void report_invariant_failure ( const std::string &  file,
const std::string &  function,
int  line,
std::string  reason,
std::string  condition,
Diagnostics &&...  diagnostics 
)

This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'.

Definition at line 354 of file invariant.h.