Include dependency graph for state.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | state_typet |
| class | initial_state_exprt |
| class | evaluate_exprt |
| class | update_state_exprt |
| class | allocate_exprt |
| class | allocate_state_exprt |
| class | reallocate_exprt |
| class | reallocate_state_exprt |
| class | deallocate_state_exprt |
| class | state_live_object_exprt |
| class | state_writeable_object_exprt |
| class | state_is_cstring_exprt |
| class | state_cstrlen_exprt |
| class | state_is_dynamic_object_exprt |
| class | state_object_size_exprt |
| class | state_ok_exprt |
| class | state_type_compatible_exprt |
| class | enter_scope_state_exprt |
| class | exit_scope_state_exprt |
Function Documentation
◆ state_expr()
|
inlinestatic |
◆ state_predicate_type()
|
inlinestatic |
◆ to_allocate_expr()
|
inline |
Cast an exprt to a allocate_exprt.
expr must be known to be allocate_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type allocate_exprt
◆ to_allocate_state_expr()
|
inline |
Cast an exprt to a allocate_state_exprt.
expr must be known to be allocate_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type allocate_state_exprt
◆ to_deallocate_state_expr()
|
inline |
Cast an exprt to a deallocate_state_exprt.
expr must be known to be deallocate_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type deallocate_state_exprt
◆ to_enter_scope_state_expr() [1/2]
|
inline |
Cast an exprt to a enter_scope_state_exprt.
expr must be known to be enter_scope_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type enter_scope_state_exprt
◆ to_enter_scope_state_expr() [2/2]
|
inline |
Cast an exprt to a enter_scope_state_exprt.
expr must be known to be enter_scope_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type enter_scope_state_exprt
◆ to_evaluate_expr() [1/2]
|
inline |
Cast an exprt to a evaluate_exprt.
expr must be known to be evaluate_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type evaluate_exprt
◆ to_evaluate_expr() [2/2]
|
inline |
Cast an exprt to a evaluate_exprt.
expr must be known to be evaluate_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type evaluate_exprt
◆ to_exit_scope_state_expr() [1/2]
|
inline |
Cast an exprt to a exit_scope_state_exprt.
expr must be known to be exit_scope_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type exit_scope_state_exprt
◆ to_exit_scope_state_expr() [2/2]
|
inline |
Cast an exprt to a exit_scope_state_exprt.
expr must be known to be exit_scope_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type exit_scope_state_exprt
◆ to_initial_state_expr() [1/2]
|
inline |
Cast an exprt to a initial_state_exprt.
expr must be known to be initial_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type initial_state_exprt
◆ to_initial_state_expr() [2/2]
|
inline |
Cast an exprt to a initial_state_exprt.
expr must be known to be initial_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type initial_state_exprt
◆ to_reallocate_expr()
|
inline |
Cast an exprt to a reallocate_exprt.
expr must be known to be reallocate_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type allocate_exprt
◆ to_reallocate_state_expr()
|
inline |
Cast an exprt to a reallocate_state_exprt.
expr must be known to be reallocate_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type reallocate_state_exprt
◆ to_state_cstrlen_expr() [1/2]
|
inline |
Cast an exprt to a state_cstrlen_exprt.
expr must be known to be state_cstrlen_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_cstrlen_exprt
◆ to_state_cstrlen_expr() [2/2]
|
inline |
Cast an exprt to a state_cstrlen_exprt.
expr must be known to be state_cstrlen_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_cstrlen_exprt
◆ to_state_is_cstring_expr() [1/2]
|
inline |
Cast an exprt to a state_is_cstring_exprt.
expr must be known to be state_is_cstring_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_is_cstring_exprt
◆ to_state_is_cstring_expr() [2/2]
|
inline |
Cast an exprt to a state_is_cstring_exprt.
expr must be known to be state_is_cstring_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_is_cstring_exprt
◆ to_state_is_dynamic_object_expr() [1/2]
|
inline |
Cast an exprt to a state_is_dynamic_object_exprt.
expr must be known to be state_is_dynamic_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_is_dynamic_object_exprt
◆ to_state_is_dynamic_object_expr() [2/2]
|
inline |
Cast an exprt to a state_is_dynamic_object_exprt.
expr must be known to be state_is_dynamic_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_is_dynamic_object_exprt
◆ to_state_live_object_expr() [1/2]
|
inline |
Cast an exprt to a state_live_object_exprt.
expr must be known to be state_live_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_live_object_exprt
◆ to_state_live_object_expr() [2/2]
|
inline |
Cast an exprt to a state_live_object_exprt.
expr must be known to be state_live_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_live_object_exprt
◆ to_state_object_size_expr() [1/2]
|
inline |
Cast an exprt to a state_object_size_exprt.
expr must be known to be state_object_size_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_object_size_exprt
◆ to_state_object_size_expr() [2/2]
|
inline |
Cast an exprt to a state_object_size_exprt.
expr must be known to be state_object_size_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_object_size_exprt
◆ to_state_ok_expr() [1/2]
|
inline |
Cast an exprt to a state_ok_exprt.
expr must be known to be state_ok_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_ok_exprt
◆ to_state_ok_expr() [2/2]
|
inline |
Cast an exprt to a state_ok_exprt.
expr must be known to be state_ok_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_ok_exprt
◆ to_state_type_compatible_expr() [1/2]
|
inline |
Cast an exprt to a state_type_compatible_exprt.
expr must be known to be state_type_compatible_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_type_compatible_exprt
◆ to_state_type_compatible_expr() [2/2]
|
inline |
Cast an exprt to a state_type_compatible_exprt.
expr must be known to be state_type_compatible_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_type_compatible_exprt
◆ to_state_writeable_object_expr() [1/2]
|
inline |
Cast an exprt to a state_writeable_object_exprt.
expr must be known to be state_writeable_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_writeable_object_exprt
◆ to_state_writeable_object_expr() [2/2]
|
inline |
Cast an exprt to a state_writeable_object_exprt.
expr must be known to be state_writeable_object_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type state_writeable_object_exprt
◆ to_update_state_expr() [1/2]
|
inline |
Cast an exprt to a update_state_exprt.
expr must be known to be update_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type update_state_exprt
◆ to_update_state_expr() [2/2]
|
inline |
Cast an exprt to a update_state_exprt.
expr must be known to be update_state_exprt.
- Parameters
-
expr Source expression
- Returns
- Object of type update_state_exprt
