cprover
|
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/prefix.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"
Go to the source code of this file.
Variables | |
std::size_t | allocate_counter = 0 |
Simplify State Expressions.
Definition in file simplify_state_expr.cpp.
|
static |
Definition at line 641 of file simplify_state_expr.cpp.
|
static |
Definition at line 647 of file simplify_state_expr.cpp.
exprt simplify_allocate | ( | allocate_exprt | src | ) |
Definition at line 180 of file simplify_state_expr.cpp.
exprt simplify_cstrlen_expr | ( | state_cstrlen_exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 757 of file simplify_state_expr.cpp.
exprt simplify_evaluate_allocate_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns ) |
Definition at line 206 of file simplify_state_expr.cpp.
exprt simplify_evaluate_deallocate_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns ) |
Definition at line 237 of file simplify_state_expr.cpp.
exprt simplify_evaluate_enter_scope_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns ) |
Definition at line 251 of file simplify_state_expr.cpp.
exprt simplify_evaluate_exit_scope_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns ) |
Definition at line 264 of file simplify_state_expr.cpp.
exprt simplify_evaluate_update | ( | evaluate_exprt | evaluate_expr, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 47 of file simplify_state_expr.cpp.
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 659 of file simplify_state_expr.cpp.
exprt simplify_is_dynamic_object_expr | ( | state_is_dynamic_object_exprt | src | ) |
Definition at line 463 of file simplify_state_expr.cpp.
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 836 of file simplify_state_expr.cpp.
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 310 of file simplify_state_expr.cpp.
Definition at line 305 of file simplify_state_expr.cpp.
Definition at line 277 of file simplify_state_expr.cpp.
exprt simplify_object_size_expr | ( | state_object_size_exprt | src, |
const namespacet & | ns ) |
Definition at line 497 of file simplify_state_expr.cpp.
exprt simplify_ok_expr | ( | state_ok_exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 525 of file simplify_state_expr.cpp.
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 945 of file simplify_state_expr.cpp.
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 894 of file simplify_state_expr.cpp.
exprt simplify_state_expr | ( | exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 1084 of file simplify_state_expr.cpp.
exprt simplify_state_expr_node | ( | exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns ) |
Definition at line 958 of file simplify_state_expr.cpp.
exprt simplify_writeable_object_expr | ( | state_writeable_object_exprt | src, |
const namespacet & | ns ) |
Definition at line 426 of file simplify_state_expr.cpp.
Definition at line 37 of file simplify_state_expr.cpp.
std::size_t allocate_counter = 0 |
Definition at line 30 of file simplify_state_expr.cpp.