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 
19 {
20  return id2string(id)+"$object";
21 }
22 
23 void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
24 {
25  if(!symbol.is_lvalue)
26  return;
27 
28  if(symbol.type.get(ID_C_failed_symbol)!="")
29  return;
30 
31  if(symbol.type.id()==ID_pointer)
32  {
33  symbolt new_symbol;
34  new_symbol.is_lvalue=true;
35  new_symbol.module=symbol.module;
36  new_symbol.mode=symbol.mode;
37  new_symbol.base_name=failed_symbol_id(symbol.base_name);
38  new_symbol.name=failed_symbol_id(symbol.name);
39  new_symbol.type=symbol.type.subtype();
40  new_symbol.value.make_nil();
41  new_symbol.type.set(ID_C_is_failed_symbol, true);
42 
43  symbol.type.set(ID_C_failed_symbol, new_symbol.name);
44 
45  if(new_symbol.type.id()==ID_pointer)
46  add_failed_symbol(new_symbol, symbol_table); // recursive call
47 
48  symbol_table.move(new_symbol);
49  }
50 }
51 
52 void add_failed_symbols(symbol_tablet &symbol_table)
53 {
54  // the symbol table iterators are not stable, and
55  // we are adding new symbols, this
56  // is why we need a list of pointers
57  typedef std::list< ::symbolt *> symbol_listt;
58  symbol_listt symbol_list;
59 
60  Forall_symbols(it, symbol_table.symbols)
61  symbol_list.push_back(&(it->second));
62 
63  for(symbol_listt::const_iterator
64  it=symbol_list.begin();
65  it!=symbol_list.end();
66  it++)
67  {
68  add_failed_symbol(**it, symbol_table);
69  }
70 }
71 
73  const symbol_exprt &expr,
74  const namespacet &ns)
75 {
76  const symbolt &symbol=ns.lookup(expr);
77  irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
78 
80  return nil_exprt();
81 
82  const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
83 
84  return symbol_exprt(failed_symbol_id, failed_symbol.type);
85 }
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
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irep_idt mode
Language mode.
Definition: symbol.h:55
exprt value
Initial value of symbol.
Definition: symbol.h:40
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Pointer Dereferencing.
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
const irep_idt & id() const
Definition: irep.h:189
symbolst symbols
Definition: symbol_table.h:57
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
The NIL expression.
Definition: std_expr.h:3764
irep_idt failed_symbol_id(const irep_idt &id)
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
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.
typet type
Type of symbol.
Definition: symbol.h:37
void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void make_nil()
Definition: irep.h:243
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void add_failed_symbols(symbol_tablet &symbol_table)
const typet & subtype() const
Definition: type.h:31
bool empty() const
Definition: dstring.h:61
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_lvalue
Definition: symbol.h:71