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  state.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  state.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: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:237
const irep_idt & id() const
Definition: irep.h:189
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
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:130
Symbolic Execution of ANSI-C.