CBMC: /home/runner/work/cbmc/cbmc/src/cprover/simplify_state_expr.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Functions | Variables

simplify_state_expr.cpp File Reference

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.

Functions

exprt simplify_state_expr_node (exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)

static bool types_are_compatible (const typet &a, const typet &b)

exprt simplify_evaluate_update (evaluate_exprt evaluate_expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

exprt simplify_allocate (allocate_exprt src)

exprt simplify_evaluate_allocate_state (evaluate_exprt evaluate_expr, const namespacet &ns)

exprt simplify_evaluate_deallocate_state (evaluate_exprt evaluate_expr, const namespacet &ns)

exprt simplify_evaluate_enter_scope_state (evaluate_exprt evaluate_expr, const namespacet &ns)

exprt simplify_evaluate_exit_scope_state (evaluate_exprt evaluate_expr, const namespacet &ns)

exprt simplify_object_expression_rec (exprt src)

exprt simplify_object_expression (exprt src)

exprt simplify_live_object_expr (state_live_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

exprt simplify_writeable_object_expr (state_writeable_object_exprt src, const namespacet &ns)

exprt simplify_is_dynamic_object_expr (state_is_dynamic_object_exprt src)

exprt simplify_object_size_expr (state_object_size_exprt src, const namespacet &ns)

exprt simplify_ok_expr (state_ok_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

static bool is_a_char_type (const typet &type)

static bool is_zero_char (const exprt &src, const namespacet &ns)

exprt simplify_is_cstring_expr (state_is_cstring_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

exprt simplify_cstrlen_expr (state_cstrlen_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

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)

exprt simplify_pointer_offset_expr (pointer_offset_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

exprt simplify_pointer_object_expr (pointer_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

exprt simplify_state_expr (exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

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 bool is_a_char_type ( const typet & type )

static

Definition at line 644 of file simplify_state_expr.cpp.

◆ is_zero_char()

static bool is_zero_char ( const exprt & src,

const namespacet & ns

)

static

Definition at line 650 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 760 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 662 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 839 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()

exprt simplify_object_expression ( exprt src )

Definition at line 304 of file simplify_state_expr.cpp.

◆ simplify_object_expression_rec()

exprt simplify_object_expression_rec ( exprt src )

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 528 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 948 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 897 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 1087 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 961 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()

static bool types_are_compatible ( const typet & a,

const typet & b

)

static

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.