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

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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 typettype )
static

Definition at line 644 of file simplify_state_expr.cpp.

◆  is_zero_char()

static bool is_zero_char ( const exprtsrc,
const namespacetns 
)
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 namespacetns 
)

Definition at line 760 of file simplify_state_expr.cpp.

◆  simplify_evaluate_allocate_state()

exprt simplify_evaluate_allocate_state ( evaluate_exprt  evaluate_expr,
const namespacetns 
)

Definition at line 205 of file simplify_state_expr.cpp.

◆  simplify_evaluate_deallocate_state()

exprt simplify_evaluate_deallocate_state ( evaluate_exprt  evaluate_expr,
const namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

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 namespacetns 
)

Definition at line 425 of file simplify_state_expr.cpp.

◆  types_are_compatible()

static bool types_are_compatible ( const typeta,
const typetb 
)
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.

AltStyle によって変換されたページ (->オリジナル) /