CBMC
|
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"
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 644 of file simplify_state_expr.cpp.
|
static |
Definition at line 650 of file simplify_state_expr.cpp.
exprt simplify_allocate | ( | allocate_exprt | src | ) |
Definition at line 179 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 760 of file simplify_state_expr.cpp.
exprt simplify_evaluate_allocate_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns | ||
) |
Definition at line 205 of file simplify_state_expr.cpp.
exprt simplify_evaluate_deallocate_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns | ||
) |
Definition at line 236 of file simplify_state_expr.cpp.
exprt simplify_evaluate_enter_scope_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns | ||
) |
Definition at line 250 of file simplify_state_expr.cpp.
exprt simplify_evaluate_exit_scope_state | ( | evaluate_exprt | evaluate_expr, |
const namespacet & | ns | ||
) |
Definition at line 263 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 46 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 662 of file simplify_state_expr.cpp.
exprt simplify_is_dynamic_object_expr | ( | state_is_dynamic_object_exprt | src | ) |
Definition at line 462 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 839 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 309 of file simplify_state_expr.cpp.
Definition at line 304 of file simplify_state_expr.cpp.
Definition at line 276 of file simplify_state_expr.cpp.
exprt simplify_object_size_expr | ( | state_object_size_exprt | src, |
const namespacet & | ns | ||
) |
Definition at line 496 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 528 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 948 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 897 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 1087 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 961 of file simplify_state_expr.cpp.
exprt simplify_writeable_object_expr | ( | state_writeable_object_exprt | src, |
const namespacet & | ns | ||
) |
Definition at line 425 of file simplify_state_expr.cpp.
Definition at line 36 of file simplify_state_expr.cpp.
std::size_t allocate_counter = 0 |
Definition at line 29 of file simplify_state_expr.cpp.