CBMC
detail Namespace Reference

Classes

struct  expr_try_dynamic_cast_return_typet
 
struct  expr_dynamic_cast_return_typet
 
struct  always_falset
 

Functions

std::string assemble_diagnostics ()
 
template<typename T >
std::string diagnostic_as_string (T &&val)
 
void write_rest_diagnostics (std::ostream &)
 
template<typename T , typename... Ts>
void write_rest_diagnostics (std::ostream &out, T &&next, Ts &&... rest)
 
template<typename... Diagnostics>
std::string assemble_diagnostics (Diagnostics &&... args)
 
template<typename Tag >
bool can_cast_side_effect_expr_impl (const exprt &expr, const Tag &tag)
 
template<typename Tag >
bool can_cast_code_impl (const exprt &expr, const Tag &tag)
 

Function Documentation

◆ assemble_diagnostics() [1/2]

std::string detail::assemble_diagnostics ( )
inline

Definition at line 342 of file invariant.h.

◆ assemble_diagnostics() [2/2]

template<typename... Diagnostics>
std::string detail::assemble_diagnostics ( Diagnostics &&...  args)

Definition at line 367 of file invariant.h.

◆ can_cast_code_impl()

template<typename Tag >
bool detail::can_cast_code_impl ( const exprt expr,
const Tag &  tag 
)
inline

Definition at line 84 of file std_code_base.h.

◆ can_cast_side_effect_expr_impl()

template<typename Tag >
bool detail::can_cast_side_effect_expr_impl ( const exprt expr,
const Tag &  tag 
)
inline

Definition at line 1487 of file std_code.h.

◆ diagnostic_as_string()

template<typename T >
std::string detail::diagnostic_as_string ( T &&  val)

Definition at line 348 of file invariant.h.

◆ write_rest_diagnostics() [1/2]

void detail::write_rest_diagnostics ( std::ostream &  )
inline

Definition at line 355 of file invariant.h.

◆ write_rest_diagnostics() [2/2]

template<typename T , typename... Ts>
void detail::write_rest_diagnostics ( std::ostream &  out,
T &&  next,
Ts &&...  rest 
)

Definition at line 360 of file invariant.h.