cprover
|
Templated functions to cast to specific exprt-derived classes. More...
#include <typeinfo>
#include <type_traits>
#include <functional>
#include "invariant.h"
#include "expr.h"
Go to the source code of this file.
Classes | |
struct | detail::expr_try_dynamic_cast_return_typet< Ret, T > |
struct | detail::expr_dynamic_cast_return_typet< Ret, T > |
Namespaces | |
detail | |
Functions | |
template<typename T > | |
bool | can_cast_expr (const exprt &base) |
Check whether a reference to a generic exprt is of a specific derived class. More... | |
template<typename T > | |
bool | can_cast_type (const typet &base) |
Check whether a reference to a generic typet is of a specific derived class. More... | |
void | validate_expr (const exprt &) |
Called after casting. More... | |
void | validate_type (const typet &) |
Called after casting. More... | |
template<typename T , typename TExpr > | |
auto | expr_try_dynamic_cast (TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type |
Try to cast a reference to a generic exprt to a specific derived class. More... | |
template<typename T , typename TType > | |
auto | type_try_dynamic_cast (TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type |
Try to cast a reference to a generic typet to a specific derived class. More... | |
template<typename T , typename TExpr > | |
auto | expr_dynamic_cast (TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type |
Cast a reference to a generic exprt to a specific derived class. More... | |
template<typename T , typename TExpr > | |
auto | expr_checked_cast (TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type |
Cast a reference to a generic exprt to a specific derived class. More... | |
template<typename T , typename TType > | |
auto | type_checked_cast (TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type |
Cast a reference to a generic typet to a specific derived class and checks that the type could be converted. More... | |
void | validate_operands (const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false) |
Templated functions to cast to specific exprt-derived classes.
Definition in file expr_cast.h.
|
inline |
Check whether a reference to a generic exprt is of a specific derived class.
Implement template specializations of this function to enable casting
T | The exprt-derived class to check for |
base | Reference to a generic exprt |
Referenced by expr_try_dynamic_cast().
|
inline |
Check whether a reference to a generic typet is of a specific derived class.
Implement template specializations of this function to enable casting
T | The typet-derived class to check for |
base | Reference to a generic typet |
Referenced by type_try_dynamic_cast().
auto expr_checked_cast | ( | TExpr & | base | ) | -> typename detail::expr_dynamic_cast_return_typet<T, TExpr>::type |
Cast a reference to a generic exprt to a specific derived class.
Also assert that the expression has the expected type.
T | The reference or const reference type to TUnderlying to cast to |
TExpr | The original type to cast from, either exprt or const exprt |
base | Reference to a generic exprt |
std::bad_cast | If base is not an instance of TUnderlying |
Definition at line 184 of file expr_cast.h.
References expr_dynamic_cast(), and PRECONDITION.
Referenced by add_dependency_to_string_subexprs(), array_poolt::of_argument(), simplify_exprt::simplify_typecast(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), string_insertion_builtin_functiont::string_insertion_builtin_functiont(), string_transformation_builtin_functiont::string_transformation_builtin_functiont(), and to_string_builtin_function().
auto expr_dynamic_cast | ( | TExpr & | base | ) | -> typename detail::expr_dynamic_cast_return_typet<T, TExpr>::type |
Cast a reference to a generic exprt to a specific derived class.
T | The reference or const reference type to TUnderlying to cast to |
TExpr | The original type to cast from, either exprt or const exprt |
base | Reference to a generic exprt |
std::bad_cast | If base is not an instance of TUnderlying |
Definition at line 165 of file expr_cast.h.
References expr_try_dynamic_cast().
Referenced by expr_checked_cast(), string_refinementt::get(), notify_static_method_calls(), and sparse_arrayt::sparse_arrayt().
auto expr_try_dynamic_cast | ( | TExpr & | base | ) | -> typename detail::expr_try_dynamic_cast_return_typet<T, TExpr>::type |
Try to cast a reference to a generic exprt to a specific derived class.
T | The reference or const reference type to TUnderlying to cast to |
TExpr | The original type to cast from, either exprt or const exprt |
base | Reference to a generic exprt |
Definition at line 91 of file expr_cast.h.
References can_cast_expr(), and validate_expr().
Referenced by add_node(), eval_string(), expr_dynamic_cast(), string_constraintt::gather_indices(), string_refinementt::get(), remove_java_newt::lower_java_new(), notify_static_method_calls(), boolbvt::set_to(), simplify_exprt::simplify_inequality(), and string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt().
auto type_checked_cast | ( | TType & | base | ) | -> typename detail::expr_dynamic_cast_return_typet<T, TType>::type |
Cast a reference to a generic typet to a specific derived class and checks that the type could be converted.
T | The reference or const reference type to TUnderlying to cast to |
TType | The original type to cast from, either typet or const typet |
base | Reference to a generic typet |
Definition at line 198 of file expr_cast.h.
References CHECK_RETURN, and type_try_dynamic_cast().
Referenced by java_class_typet::get_annotations(), boolbv_widtht::get_entry(), and java_qualifierst::write().
auto type_try_dynamic_cast | ( | TType & | base | ) | -> typename detail::expr_try_dynamic_cast_return_typet<T, TType>::type |
Try to cast a reference to a generic typet to a specific derived class.
T | The reference or const reference type to TUnderlying to cast to |
TType | The original type to cast from, either typet or const typet |
base | Reference to a generic typet |
Definition at line 119 of file expr_cast.h.
References can_cast_type(), and validate_type().
Referenced by type_checked_cast().
|
inline |
Called after casting.
Provides a point to assert on the structure of the expr. By default, this is a no-op, but you can provide an overload to validate particular types. Should always succeed unless the program has entered an invalid state. We validate objects at cast time as that is when these checks have been used historically, but it would be reasonable to validate objects in this way at any time.
Definition at line 49 of file expr_cast.h.
Referenced by expr_try_dynamic_cast().
|
inline |
Definition at line 206 of file expr_cast.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by validate_expr().
|
inline |
Called after casting.
Provides a point to check data invariants on the structure of the typet. By default, this is a no-op, but you can provide an overload to validate particular types. Should always succeed unless the program has entered an invalid state. We validate objects at cast time as that is when these checks have been used historically, but it would be reasonable to validate objects in this way at any time.
Definition at line 57 of file expr_cast.h.
Referenced by type_try_dynamic_cast().