cprover
Loading...
Searching...
No Matches
symex_dereference_state.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/symbol_table.h>
15
30const symbolt *
32{
33 if(is_ssa_expr(expr))
34 {
35 const ssa_exprt &ssa_expr=to_ssa_expr(expr);
36 if(ssa_expr.get_original_expr().id()!=ID_symbol)
37 return nullptr;
38
39 const symbolt &ptr_symbol=
40 ns.lookup(to_ssa_expr(expr).get_object_name());
41
42 const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
43
44 const symbolt *symbol;
45 if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
46 {
47 symbolt sym=*symbol;
48 symbolt *sym_ptr=nullptr;
49 const ssa_exprt sym_expr =
50 state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
51 sym.name = sym_expr.get_identifier();
52 state.symbol_table.move(sym, sym_ptr);
53 return sym_ptr;
54 }
55 }
56 else if(expr.id()==ID_symbol)
57 {
58 const symbolt &ptr_symbol=
60
61 const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
62
63 const symbolt *symbol;
64 if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
65 {
66 symbolt sym=*symbol;
67 symbolt *sym_ptr=nullptr;
68 const ssa_exprt sym_expr =
69 state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
70 sym.name = sym_expr.get_identifier();
71 state.symbol_table.move(sym, sym_ptr);
72 return sym_ptr;
73 }
74 }
75
76 return nullptr;
77}
78
80std::vector<exprt>
82{
83 return state.value_set.get_value_set(expr, ns);
84}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
const irep_idt & get_identifier() const
Definition: std_expr.h:109
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
std::vector< exprt > get_value_set(const exprt &expr) const override
Just forwards a value-set query to state.value_set
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:354
@ L1
Definition: renamed.h:24
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
Author: Diffblue Ltd.
Symbolic Execution of ANSI-C.