Simplify State Expressions. More...
#include "simplify_state_expr.h"#include <util/arith_tools.h>#include <util/c_types.h>#include <util/expr_util.h>#include <util/namespace.h>#include <util/pointer_offset_size.h>#include <util/pointer_predicates.h>#include <util/simplify_expr.h>#include <util/std_expr.h>#include <util/symbol.h>#include "may_alias.h"#include "may_be_same_object.h"#include "sentinel_dll.h"#include "state.h"
Include dependency graph for simplify_state_expr.cpp:Go to the source code of this file.
Variables | |
| std::size_t | allocate_counter = 0 |
Detailed Description
Simplify State Expressions.
Definition in file simplify_state_expr.cpp.
Function Documentation
◆ is_a_char_type()
|
static |
Definition at line 640 of file simplify_state_expr.cpp.
◆ is_zero_char()
|
static |
Definition at line 646 of file simplify_state_expr.cpp.
◆ simplify_allocate()
| exprt simplify_allocate | ( | allocate_exprt | src | ) |
Definition at line 179 of file simplify_state_expr.cpp.
◆ simplify_cstrlen_expr()
| exprt simplify_cstrlen_expr | ( | state_cstrlen_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 756 of file simplify_state_expr.cpp.
◆ simplify_evaluate_allocate_state()
| exprt simplify_evaluate_allocate_state | ( | evaluate_exprt | evaluate_expr, |
| const namespacet & | ns | ||
| ) |
Definition at line 205 of file simplify_state_expr.cpp.
◆ simplify_evaluate_deallocate_state()
| exprt simplify_evaluate_deallocate_state | ( | evaluate_exprt | evaluate_expr, |
| const namespacet & | ns | ||
| ) |
Definition at line 236 of file simplify_state_expr.cpp.
◆ simplify_evaluate_enter_scope_state()
| exprt simplify_evaluate_enter_scope_state | ( | evaluate_exprt | evaluate_expr, |
| const namespacet & | ns | ||
| ) |
Definition at line 250 of file simplify_state_expr.cpp.
◆ simplify_evaluate_exit_scope_state()
| exprt simplify_evaluate_exit_scope_state | ( | evaluate_exprt | evaluate_expr, |
| const namespacet & | ns | ||
| ) |
Definition at line 263 of file simplify_state_expr.cpp.
◆ simplify_evaluate_update()
| exprt simplify_evaluate_update | ( | evaluate_exprt | evaluate_expr, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 46 of file simplify_state_expr.cpp.
◆ simplify_is_cstring_expr()
| exprt simplify_is_cstring_expr | ( | state_is_cstring_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 658 of file simplify_state_expr.cpp.
◆ simplify_is_dynamic_object_expr()
| exprt simplify_is_dynamic_object_expr | ( | state_is_dynamic_object_exprt | src | ) |
Definition at line 462 of file simplify_state_expr.cpp.
◆ simplify_is_sentinel_dll_expr()
| exprt simplify_is_sentinel_dll_expr | ( | state_is_sentinel_dll_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 835 of file simplify_state_expr.cpp.
◆ simplify_live_object_expr()
| exprt simplify_live_object_expr | ( | state_live_object_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 309 of file simplify_state_expr.cpp.
◆ simplify_object_expression()
Definition at line 304 of file simplify_state_expr.cpp.
◆ simplify_object_expression_rec()
Definition at line 276 of file simplify_state_expr.cpp.
◆ simplify_object_size_expr()
| exprt simplify_object_size_expr | ( | state_object_size_exprt | src, |
| const namespacet & | ns | ||
| ) |
Definition at line 496 of file simplify_state_expr.cpp.
◆ simplify_ok_expr()
| exprt simplify_ok_expr | ( | state_ok_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 524 of file simplify_state_expr.cpp.
◆ simplify_pointer_object_expr()
| exprt simplify_pointer_object_expr | ( | pointer_object_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 944 of file simplify_state_expr.cpp.
◆ simplify_pointer_offset_expr()
| exprt simplify_pointer_offset_expr | ( | pointer_offset_exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 893 of file simplify_state_expr.cpp.
◆ simplify_state_expr()
| exprt simplify_state_expr | ( | exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 1083 of file simplify_state_expr.cpp.
◆ simplify_state_expr_node()
| exprt simplify_state_expr_node | ( | exprt | src, |
| const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 957 of file simplify_state_expr.cpp.
◆ simplify_writeable_object_expr()
| exprt simplify_writeable_object_expr | ( | state_writeable_object_exprt | src, |
| const namespacet & | ns | ||
| ) |
Definition at line 425 of file simplify_state_expr.cpp.
◆ types_are_compatible()
Definition at line 36 of file simplify_state_expr.cpp.
Variable Documentation
◆ allocate_counter
| std::size_t allocate_counter = 0 |
Definition at line 29 of file simplify_state_expr.cpp.
