cprover
add_failed_symbols.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Dereferencing
4
5Author: 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>
18
19#include <list>
20
26{
27 return id2string(id)+"$object";
28}
29
34void 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
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
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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:48
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.
Symbol table entry.
Author: Diffblue Ltd.