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)!="")
68  return;
69 
70  add_failed_symbol(*symbol_table.get_writeable(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 
95  const symbol_exprt &expr,
96  const namespacet &ns)
97 {
98  const symbolt &symbol=ns.lookup(expr);
99  irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
100 
101  if(failed_symbol_id.empty())
102  return nil_exprt();
103 
104  const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
105 
106  return symbol_exprt(failed_symbol_id, failed_symbol.type);
107 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
irep_idt mode
Language mode.
Definition: symbol.h:52
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
Definition: symbol.h:37
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
Pointer Dereferencing.
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, an lvalue, and doesn&#39;t already have one.
const irep_idt & id() const
Definition: irep.h:189
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
The NIL expression.
Definition: std_expr.h:4510
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...
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
const symbolst & symbols
typet type
Type of symbol.
Definition: symbol.h:34
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...
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
void make_nil()
Definition: irep.h:243
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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...
const typet & subtype() const
Definition: type.h:33
bool empty() const
Definition: dstring.h:61
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_lvalue
Definition: symbol.h:68