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 &property,
18  const std::string &msg,
19  const guardt &guard)
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=
40  ptr_symbol.type.get("#failed_symbol");
41 
42  if(failed_symbol!="" &&
43  !ns.lookup(failed_symbol, symbol))
44  {
45  symbolt sym=*symbol;
46  symbolt *sym_ptr=nullptr;
47  symbol_exprt sym_expr=sym.symbol_expr();
48  state.rename(sym_expr, ns, goto_symex_statet::L1);
49  sym.name=to_ssa_expr(sym_expr).get_identifier();
50  goto_symex.new_symbol_table.move(sym, sym_ptr);
51  symbol=sym_ptr;
52  return true;
53  }
54  }
55  else if(expr.id()==ID_symbol)
56  {
57  const symbolt &ptr_symbol=
58  ns.lookup(to_symbol_expr(expr).get_identifier());
59 
60  const irep_idt &failed_symbol=
61  ptr_symbol.type.get("#failed_symbol");
62 
63  if(failed_symbol!="" &&
64  !ns.lookup(failed_symbol, symbol))
65  {
66  symbolt sym=*symbol;
67  symbolt *sym_ptr=nullptr;
68  symbol_exprt sym_expr=sym.symbol_expr();
69  state.rename(sym_expr, ns, goto_symex_statet::L1);
70  sym.name=to_ssa_expr(sym_expr).get_identifier();
71  goto_symex.new_symbol_table.move(sym, sym_ptr);
72  symbol=sym_ptr;
73  return true;
74  }
75  }
76 
77  return false;
78 }
79 
81  const exprt &expr,
82  value_setst::valuest &value_set)
83 {
84  state.value_set.get_value_set(expr, value_set, goto_symex.ns);
85 
86  #if 0
87  std::cout << "**************************\n";
88  state.value_set.output(goto_symex.ns, std::cout);
89  std::cout << "**************************\n";
90  #endif
91 
92  #if 0
93  std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n';
94  #endif
95 
96  #if 0
97  std::cout << "**************************\n";
98  for(value_setst::valuest::const_iterator it=value_set.begin();
99  it!=value_set.end();
100  it++)
101  std::cout << from_expr(goto_symex.ns, "", *it) << '\n';
102  std::cout << "**************************\n";
103  #endif
104 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
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
Definition: value_set.cpp:314
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:33
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const irep_idt & id() const
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
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:62
Symbol table.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
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)
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
typet type
Type of symbol.
Definition: symbol.h:37
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set.cpp:97
std::list< exprt > valuest
Definition: value_sets.h:28
const namespacet & ns
Definition: goto_symex.h:104
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Symbolic Execution of ANSI-C.