cprover
symex_dereference_state.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/symbol_table.h>
15 
30 const 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=
59  ns.lookup(to_symbol_expr(expr).get_identifier());
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 
80 std::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
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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:353
@ L1
Definition: renamed.h:24
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
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.