cprover
Loading...
Searching...
No Matches
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);
95
97 return {};
98
100
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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().
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
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
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
API to expression classes.
Symbol table entry.
Author: Diffblue Ltd.