cprover
add_failed_symbols.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Dereferencing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "add_failed_symbols.h"
13 
14 #include <util/symbol_table.h>
15 #include <util/namespace.h>
16 #include <util/std_expr.h>
17 
18 #include <list>
19 
25 {
26  return id2string(id)+"$object";
27 }
28 
33 void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
34 {
35  if(symbol.type.id()==ID_pointer)
36  {
37  symbolt new_symbol;
38  new_symbol.is_lvalue=true;
39  new_symbol.module=symbol.module;
40  new_symbol.mode=symbol.mode;
41  new_symbol.base_name=failed_symbol_id(symbol.base_name);
42  new_symbol.name=failed_symbol_id(symbol.name);
43  new_symbol.type=symbol.type.subtype();
44  new_symbol.value.make_nil();
45  new_symbol.type.set(ID_C_is_failed_symbol, true);
46 
47  symbol.type.set(ID_C_failed_symbol, new_symbol.name);
48 
49  if(new_symbol.type.id()==ID_pointer)
50  add_failed_symbol(new_symbol, symbol_table); // recursive call
51 
52  symbol_table.insert(std::move(new_symbol));
53  }
54 }
55 
62  const symbolt &symbol, symbol_table_baset &symbol_table)
63 {
64  if(!symbol.is_lvalue)
65  return;
66 
67  if(!symbol.type.get(ID_C_failed_symbol).empty())
68  return;
69 
70  add_failed_symbol(symbol_table.get_writeable_ref(symbol.name), symbol_table);
71 }
72 
77 {
78  // the symbol table iterators are not stable, and
79  // we are adding new symbols, this
80  // is why we need a list of pointers
81  std::list<const symbolt *> symbol_list;
82  for(auto &named_symbol : symbol_table.symbols)
83  symbol_list.push_back(&(named_symbol.second));
84 
85  for(const symbolt *symbol : symbol_list)
86  add_failed_symbol_if_needed(*symbol, symbol_table);
87 }
88 
90 get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
91 {
92  const symbolt &symbol=ns.lookup(expr);
93  irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
94 
96  return {};
97 
98  const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
99 
100  return symbol_exprt(failed_symbol_id, failed_symbol.type);
101 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
get_failed_symbol
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Definition: add_failed_symbols.cpp:90
typet::subtype
const typet & subtype() const
Definition: type.h:47
add_failed_symbol
void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
Create a failed-dereference symbol for the given base symbol if it is pointer-typed; if not,...
Definition: add_failed_symbols.cpp:33
irept::make_nil
void make_nil()
Definition: irep.h:475
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
failed_symbol_id
irep_idt failed_symbol_id(const irep_idt &id)
Get the name of the special symbol used to denote an unknown referee pointed to by a given pointer-ty...
Definition: add_failed_symbols.cpp:24
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
add_failed_symbol_if_needed
void add_failed_symbol_if_needed(const symbolt &symbol, symbol_table_baset &symbol_table)
Create a failed-dereference symbol for the given base symbol if it is pointer-typed,...
Definition: add_failed_symbols.cpp:61
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
add_failed_symbols.h
Pointer Dereferencing.
add_failed_symbols
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Definition: add_failed_symbols.cpp:76
symbol_table.h
Author: Diffblue Ltd.
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
API to expression classes.
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40