CBMC
|
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) |
|
inline |
Definition at line 342 of file invariant.h.
std::string detail::assemble_diagnostics | ( | Diagnostics &&... | args | ) |
Definition at line 367 of file invariant.h.
|
inline |
Definition at line 84 of file std_code_base.h.
|
inline |
Definition at line 1487 of file std_code.h.
std::string detail::diagnostic_as_string | ( | T && | val | ) |
Definition at line 348 of file invariant.h.
|
inline |
Definition at line 355 of file invariant.h.
void detail::write_rest_diagnostics | ( | std::ostream & | out, |
T && | next, | ||
Ts &&... | rest | ||
) |
Definition at line 360 of file invariant.h.