CBMC
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 
28 const symbolt *
30 {
31  if(is_ssa_expr(expr))
32  {
33  const ssa_exprt &ssa_expr=to_ssa_expr(expr);
34  if(ssa_expr.get_original_expr().id()!=ID_symbol)
35  return nullptr;
36 
37  const symbolt &ptr_symbol=
38  ns.lookup(to_ssa_expr(expr).get_object_name());
39 
40  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
41 
42  const symbolt *symbol;
43  if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
44  {
45  symbolt sym=*symbol;
46  symbolt *sym_ptr=nullptr;
47  const ssa_exprt sym_expr =
48  state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
49  sym.name = sym_expr.get_identifier();
50  state.symbol_table.move(sym, sym_ptr);
51  return sym_ptr;
52  }
53  }
54  else if(expr.id()==ID_symbol)
55  {
56  const symbolt &ptr_symbol=
57  ns.lookup(to_symbol_expr(expr).get_identifier());
58 
59  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
60 
61  const symbolt *symbol;
62  if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
63  {
64  symbolt sym=*symbol;
65  symbolt *sym_ptr=nullptr;
66  const ssa_exprt sym_expr =
67  state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
68  sym.name = sym_expr.get_identifier();
69  state.symbol_table.move(sym, sym_ptr);
70  return sym_ptr;
71  }
72  }
73 
74  return nullptr;
75 }
76 
78 std::vector<exprt>
80 {
81  return state.value_set.get_value_set(expr, ns);
82 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
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.
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:44
const irep_idt & id() const
Definition: irep.h:384
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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:160
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:391
@ 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:272
Symbolic Execution of ANSI-C.