|
template<> |
bool | can_cast_type< pointer_typet > (const typet &type) |
| Check whether a reference to a typet is a pointer_typet.
|
|
const pointer_typet & | to_pointer_type (const typet &type) |
| Cast a typet to a pointer_typet.
|
|
pointer_typet & | to_pointer_type (typet &type) |
| Cast a typet to a pointer_typet.
|
|
bool | is_void_pointer (const typet &type) |
| This method tests, if the given typet is a pointer of type void.
|
|
template<> |
bool | can_cast_type< reference_typet > (const typet &type) |
| Check whether a reference to a typet is a reference_typet.
|
|
const reference_typet & | to_reference_type (const typet &type) |
| Cast a typet to a reference_typet.
|
|
reference_typet & | to_reference_type (typet &type) |
| Cast a typet to a reference_typet.
|
|
bool | is_reference (const typet &type) |
| Returns true if the type is a reference.
|
|
bool | is_rvalue_reference (const typet &type) |
| Returns if the type is an R value reference.
|
|
template<> |
bool | can_cast_expr< object_descriptor_exprt > (const exprt &base) |
|
void | validate_expr (const object_descriptor_exprt &value) |
|
const object_descriptor_exprt & | to_object_descriptor_expr (const exprt &expr) |
| Cast an exprt to an object_descriptor_exprt.
|
|
object_descriptor_exprt & | to_object_descriptor_expr (exprt &expr) |
| Cast an exprt to an object_descriptor_exprt.
|
|
template<> |
bool | can_cast_expr< dynamic_object_exprt > (const exprt &base) |
|
void | validate_expr (const dynamic_object_exprt &value) |
|
const dynamic_object_exprt & | to_dynamic_object_expr (const exprt &expr) |
| Cast an exprt to a dynamic_object_exprt.
|
|
dynamic_object_exprt & | to_dynamic_object_expr (exprt &expr) |
| Cast an exprt to a dynamic_object_exprt.
|
|
template<> |
bool | can_cast_expr< is_dynamic_object_exprt > (const exprt &base) |
|
void | validate_expr (const is_dynamic_object_exprt &value) |
|
const is_dynamic_object_exprt & | to_is_dynamic_object_expr (const exprt &expr) |
|
is_dynamic_object_exprt & | to_is_dynamic_object_expr (exprt &expr) |
|
template<> |
bool | can_cast_expr< pointer_in_range_exprt > (const exprt &base) |
|
void | validate_expr (const pointer_in_range_exprt &value) |
|
const pointer_in_range_exprt & | to_pointer_in_range_expr (const exprt &expr) |
|
pointer_in_range_exprt & | to_pointer_in_range_expr (exprt &expr) |
|
template<> |
bool | can_cast_expr< prophecy_pointer_in_range_exprt > (const exprt &base) |
|
void | validate_expr (const prophecy_pointer_in_range_exprt &value) |
|
const prophecy_pointer_in_range_exprt & | to_prophecy_pointer_in_range_expr (const exprt &expr) |
|
prophecy_pointer_in_range_exprt & | to_prophecy_pointer_in_range_expr (exprt &expr) |
|
template<> |
bool | can_cast_expr< address_of_exprt > (const exprt &base) |
|
void | validate_expr (const address_of_exprt &value) |
|
const address_of_exprt & | to_address_of_expr (const exprt &expr) |
| Cast an exprt to an address_of_exprt.
|
|
address_of_exprt & | to_address_of_expr (exprt &expr) |
| Cast an exprt to an address_of_exprt.
|
|
template<> |
bool | can_cast_expr< object_address_exprt > (const exprt &base) |
|
void | validate_expr (const object_address_exprt &value) |
|
const object_address_exprt & | to_object_address_expr (const exprt &expr) |
| Cast an exprt to an object_address_exprt.
|
|
object_address_exprt & | to_object_address_expr (exprt &expr) |
| Cast an exprt to an object_address_exprt.
|
|
template<> |
bool | can_cast_expr< field_address_exprt > (const exprt &expr) |
|
void | validate_expr (const field_address_exprt &value) |
|
const field_address_exprt & | to_field_address_expr (const exprt &expr) |
| Cast an exprt to an field_address_exprt.
|
|
field_address_exprt & | to_field_address_expr (exprt &expr) |
| Cast an exprt to an field_address_exprt.
|
|
template<> |
bool | can_cast_expr< element_address_exprt > (const exprt &expr) |
|
void | validate_expr (const element_address_exprt &value) |
|
const element_address_exprt & | to_element_address_expr (const exprt &expr) |
| Cast an exprt to an element_address_exprt.
|
|
element_address_exprt & | to_element_address_expr (exprt &expr) |
| Cast an exprt to an element_address_exprt.
|
|
template<> |
bool | can_cast_expr< dereference_exprt > (const exprt &base) |
|
void | validate_expr (const dereference_exprt &value) |
|
const dereference_exprt & | to_dereference_expr (const exprt &expr) |
| Cast an exprt to a dereference_exprt.
|
|
dereference_exprt & | to_dereference_expr (exprt &expr) |
| Cast an exprt to a dereference_exprt.
|
|
template<> |
bool | can_cast_expr< r_or_w_ok_exprt > (const exprt &base) |
|
void | validate_expr (const r_or_w_ok_exprt &value) |
|
const r_or_w_ok_exprt & | to_r_or_w_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< r_ok_exprt > (const exprt &base) |
|
void | validate_expr (const r_ok_exprt &value) |
|
const r_ok_exprt & | to_r_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< w_ok_exprt > (const exprt &base) |
|
void | validate_expr (const w_ok_exprt &value) |
|
const w_ok_exprt & | to_w_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< prophecy_r_or_w_ok_exprt > (const exprt &base) |
|
void | validate_expr (const prophecy_r_or_w_ok_exprt &value) |
|
const prophecy_r_or_w_ok_exprt & | to_prophecy_r_or_w_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< prophecy_r_ok_exprt > (const exprt &base) |
|
void | validate_expr (const prophecy_r_ok_exprt &value) |
|
const prophecy_r_ok_exprt & | to_prophecy_r_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< prophecy_w_ok_exprt > (const exprt &base) |
|
void | validate_expr (const prophecy_w_ok_exprt &value) |
|
const prophecy_w_ok_exprt & | to_prophecy_w_ok_expr (const exprt &expr) |
|
template<> |
bool | can_cast_expr< annotated_pointer_constant_exprt > (const exprt &base) |
|
void | validate_expr (const annotated_pointer_constant_exprt &value) |
|
const annotated_pointer_constant_exprt & | to_annotated_pointer_constant_expr (const exprt &expr) |
| Cast an exprt to an annotated_pointer_constant_exprt.
|
|
annotated_pointer_constant_exprt & | to_annotated_pointer_constant_expr (exprt &expr) |
| Cast an exprt to an annotated_pointer_constant_exprt.
|
|
template<> |
bool | can_cast_expr< pointer_offset_exprt > (const exprt &base) |
|
void | validate_expr (const pointer_offset_exprt &value) |
|
const pointer_offset_exprt & | to_pointer_offset_expr (const exprt &expr) |
| Cast an exprt to a pointer_offset_exprt.
|
|
pointer_offset_exprt & | to_pointer_offset_expr (exprt &expr) |
| Cast an exprt to a pointer_offset_exprt.
|
|
template<> |
bool | can_cast_expr< pointer_object_exprt > (const exprt &base) |
|
void | validate_expr (const pointer_object_exprt &value) |
|
const pointer_object_exprt & | to_pointer_object_expr (const exprt &expr) |
| Cast an exprt to a pointer_object_exprt.
|
|
pointer_object_exprt & | to_pointer_object_expr (exprt &expr) |
| Cast an exprt to a pointer_object_exprt.
|
|
const object_size_exprt & | to_object_size_expr (const exprt &expr) |
| Cast an exprt to a object_size_exprt.
|
|
object_size_exprt & | to_object_size_expr (exprt &expr) |
| Cast an exprt to a object_size_exprt.
|
|
template<> |
bool | can_cast_expr< object_size_exprt > (const exprt &base) |
|
void | validate_expr (const object_size_exprt &value) |
|
template<> |
bool | can_cast_expr< is_cstring_exprt > (const exprt &base) |
|
void | validate_expr (const is_cstring_exprt &value) |
|
const is_cstring_exprt & | to_is_cstring_expr (const exprt &expr) |
| Cast an exprt to a is_cstring_exprt.
|
|
is_cstring_exprt & | to_is_cstring_expr (exprt &expr) |
| Cast an exprt to a is_cstring_exprt.
|
|
template<> |
bool | can_cast_expr< cstrlen_exprt > (const exprt &base) |
|
void | validate_expr (const cstrlen_exprt &value) |
|
const cstrlen_exprt & | to_cstrlen_expr (const exprt &expr) |
| Cast an exprt to a cstrlen_exprt.
|
|
cstrlen_exprt & | to_cstrlen_expr (exprt &expr) |
| Cast an exprt to a cstrlen_exprt.
|
|
template<> |
bool | can_cast_expr< live_object_exprt > (const exprt &base) |
|
void | validate_expr (const live_object_exprt &value) |
|
const live_object_exprt & | to_live_object_expr (const exprt &expr) |
| Cast an exprt to a live_object_exprt.
|
|
live_object_exprt & | to_live_object_expr (exprt &expr) |
| Cast an exprt to a live_object_exprt.
|
|
template<> |
bool | can_cast_expr< writeable_object_exprt > (const exprt &base) |
|
void | validate_expr (const writeable_object_exprt &value) |
|
const writeable_object_exprt & | to_writeable_object_expr (const exprt &expr) |
| Cast an exprt to a writeable_object_exprt.
|
|
writeable_object_exprt & | to_writeable_object_expr (exprt &expr) |
| Cast an exprt to a writeable_object_exprt.
|
|
template<> |
bool | can_cast_expr< separate_exprt > (const exprt &base) |
|
void | validate_expr (const separate_exprt &value) |
|
const separate_exprt & | to_separate_expr (const exprt &expr) |
| Cast an exprt to a separate_exprt.
|
|
separate_exprt & | to_separate_expr (exprt &expr) |
| Cast an exprt to a separate_exprt.
|
|