cprover
expr_cast.h File Reference

Templated functions to cast to specific exprt-derived classes. More...

#include <typeinfo>
#include <type_traits>
#include <functional>
#include "invariant.h"
#include "expr.h"
+ Include dependency graph for expr_cast.h:
+ This graph shows which files directly or indirectly include this file:

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)
 

Detailed Description

Templated functions to cast to specific exprt-derived classes.

Definition in file expr_cast.h.

Function Documentation

◆ can_cast_expr()

template<typename T >
bool can_cast_expr ( const exprt base)
inline

Check whether a reference to a generic exprt is of a specific derived class.

Implement template specializations of this function to enable casting

Template Parameters
TThe exprt-derived class to check for
Parameters
baseReference to a generic exprt
Returns
true if base is of type T

◆ can_cast_type()

template<typename T >
bool can_cast_type ( const typet base)
inline

Check whether a reference to a generic typet is of a specific derived class.

Implement template specializations of this function to enable casting

Template Parameters
TThe typet-derived class to check for
Parameters
baseReference to a generic typet
Returns
true if base is of type T

◆ expr_checked_cast()

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.

Also assert that the expression has the expected type.

Template Parameters
TThe reference or const reference type to TUnderlying to cast to
TExprThe original type to cast from, either exprt or const exprt
Parameters
baseReference to a generic exprt
Returns
Reference to object of type T
Exceptions
std::bad_castIf base is not an instance of TUnderlying
Remarks
If CBMC assertions (PRECONDITION) are set to abort then this will abort rather than throw if base is not an instance of TUnderlying

Definition at line 184 of file expr_cast.h.

◆ expr_dynamic_cast()

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.

Template Parameters
TThe reference or const reference type to TUnderlying to cast to
TExprThe original type to cast from, either exprt or const exprt
Parameters
baseReference to a generic exprt
Returns
Reference to object of type T
Exceptions
std::bad_castIf base is not an instance of TUnderlying

Definition at line 165 of file expr_cast.h.

◆ expr_try_dynamic_cast()

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.

Template Parameters
TThe reference or const reference type to TUnderlying to cast to
TExprThe original type to cast from, either exprt or const exprt
Parameters
baseReference to a generic exprt
Returns
Ptr to object of type TUnderlying or nullptr if base is not an instance of TUnderlying

Definition at line 91 of file expr_cast.h.

◆ type_checked_cast()

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.

Template Parameters
TThe reference or const reference type to TUnderlying to cast to
TTypeThe original type to cast from, either typet or const typet
Parameters
baseReference to a generic typet
Returns
Reference to object of type T

Definition at line 198 of file expr_cast.h.

◆ type_try_dynamic_cast()

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.

Template Parameters
TThe reference or const reference type to TUnderlying to cast to
TTypeThe original type to cast from, either typet or const typet
Parameters
baseReference to a generic typet
Returns
Ptr to object of type TUnderlying or nullptr if base is not an instance of TUnderlying

Definition at line 119 of file expr_cast.h.

◆ validate_expr()

void validate_expr ( const exprt )
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.

◆ validate_operands()

void validate_operands ( const exprt value,
exprt::operandst::size_type  number,
const char *  message,
bool  allow_more = false 
)
inline

Definition at line 206 of file expr_cast.h.

◆ validate_type()

void validate_type ( const typet )
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.