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 
17  const std::string &,
18  const std::string &,
19  const guardt &)
20 {
21 }
22 
24  const exprt &expr,
25  const symbolt *&symbol)
26 {
27  const namespacet &ns=goto_symex.ns;
28 
29  if(expr.id()==ID_symbol &&
30  expr.get_bool(ID_C_SSA_symbol))
31  {
32  const ssa_exprt &ssa_expr=to_ssa_expr(expr);
33  if(ssa_expr.get_original_expr().id()!=ID_symbol)
34  return false;
35 
36  const symbolt &ptr_symbol=
37  ns.lookup(to_ssa_expr(expr).get_object_name());
38 
39  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
40 
41  if(failed_symbol!="" &&
42  !ns.lookup(failed_symbol, symbol))
43  {
44  symbolt sym=*symbol;
45  symbolt *sym_ptr=nullptr;
46  symbol_exprt sym_expr=sym.symbol_expr();
47  state.rename(sym_expr, ns, goto_symex_statet::L1);
48  sym.name=to_ssa_expr(sym_expr).get_identifier();
49  state.symbol_table.move(sym, sym_ptr);
50  symbol=sym_ptr;
51  return true;
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  if(failed_symbol!="" &&
62  !ns.lookup(failed_symbol, symbol))
63  {
64  symbolt sym=*symbol;
65  symbolt *sym_ptr=nullptr;
66  symbol_exprt sym_expr=sym.symbol_expr();
67  state.rename(sym_expr, ns, goto_symex_statet::L1);
68  sym.name=to_ssa_expr(sym_expr).get_identifier();
69  state.symbol_table.move(sym, sym_ptr);
70  symbol=sym_ptr;
71  return true;
72  }
73  }
74 
75  return false;
76 }
77 
79  const exprt &expr,
80  value_setst::valuest &value_set)
81 {
82  state.value_set.get_value_set(expr, value_set, goto_symex.ns);
83 
84  #if 0
85  std::cout << "**************************\n";
86  state.value_set.output(goto_symex.ns, std::cout);
87  std::cout << "**************************\n";
88  #endif
89 
90  #if 0
91  std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n';
92  #endif
93 
94  #if 0
95  std::cout << "**************************\n";
96  for(value_setst::valuest::const_iterator it=value_set.begin();
97  it!=value_set.end();
98  it++)
99  std::cout << from_expr(goto_symex.ns, "", *it) << '\n';
100  std::cout << "**************************\n";
101  #endif
102 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:313
Definition: guard.h:19
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
typet type
Type of symbol.
Definition: symbol.h:34
Base class for all expressions.
Definition: expr.h:42
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:96
std::list< exprt > valuest
Definition: value_sets.h:28
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Symbolic Execution of ANSI-C.