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/namespace.h>
15 #include <util/std_expr.h>
16 #include <util/symbol.h>
17 #include <util/symbol_table_base.h>
18 
19 #include <list>
20 
26 {
27  return id2string(id)+"$object";
28 }
29 
34 void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
35 {
36  if(symbol.type.id()==ID_pointer)
37  {
38  symbolt new_symbol;
39  new_symbol.is_lvalue=true;
40  new_symbol.module=symbol.module;
41  new_symbol.mode=symbol.mode;
42  new_symbol.base_name=failed_symbol_id(symbol.base_name);
43  new_symbol.name=failed_symbol_id(symbol.name);
44  new_symbol.type=symbol.type.subtype();
45  new_symbol.value.make_nil();
46  new_symbol.type.set(ID_C_is_failed_symbol, true);
47 
48  symbol.type.set(ID_C_failed_symbol, new_symbol.name);
49 
50  if(new_symbol.type.id()==ID_pointer)
51  add_failed_symbol(new_symbol, symbol_table); // recursive call
52 
53  symbol_table.insert(std::move(new_symbol));
54  }
55 }
56 
63  const symbolt &symbol, symbol_table_baset &symbol_table)
64 {
65  if(!symbol.is_lvalue)
66  return;
67 
68  if(!symbol.type.get(ID_C_failed_symbol).empty())
69  return;
70 
71  add_failed_symbol(symbol_table.get_writeable_ref(symbol.name), symbol_table);
72 }
73 
78 {
79  // the symbol table iterators are not stable, and
80  // we are adding new symbols, this
81  // is why we need a list of pointers
82  std::list<const symbolt *> symbol_list;
83  for(auto &named_symbol : symbol_table.symbols)
84  symbol_list.push_back(&(named_symbol.second));
85 
86  for(const symbolt *symbol : symbol_list)
87  add_failed_symbol_if_needed(*symbol, symbol_table);
88 }
89 
91 get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
92 {
93  const symbolt &symbol=ns.lookup(expr);
94  irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
95 
97  return {};
98 
99  const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
100 
101  return symbol_exprt(failed_symbol_id, failed_symbol.type);
102 }
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,...
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
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....
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,...
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...
Pointer Dereferencing.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
const typet & subtype() const
Definition: type.h:47
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.
Symbol table entry.
Author: Diffblue Ltd.