cprover
symbol.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_SYMBOL_H
11#define CPROVER_UTIL_SYMBOL_H
12
17
18#include <iosfwd>
19
20#include "expr.h"
21#include "invariant.h"
22
28{
29public:
32
35
38
41
44
47
50
53
55 const irep_idt &display_name() const
56 {
58 }
59
60 // global use
63
64 // ANSI-C
68
70 {
71 clear();
72 }
73
75 void clear()
76 {
77 type.make_nil();
80
82
88 }
89
90 void swap(symbolt &b);
91 void show(std::ostream &out) const;
92
93 class symbol_exprt symbol_expr() const;
94
95 bool is_shared() const
96 {
97 return !is_thread_local;
98 }
99
100 bool is_function() const
101 {
102 return !is_type && !is_macro && type.id()==ID_code;
103 }
104
107 bool is_compiled() const
108 {
109 return type.id() == ID_code && value == exprt(ID_compiled);
110 }
111
115 {
116 PRECONDITION(type.id() == ID_code);
117 value = exprt(ID_compiled);
118 }
119
121 bool is_well_formed() const;
122
123 bool operator==(const symbolt &other) const;
124 bool operator!=(const symbolt &other) const;
125};
126
127std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
128
133{
134public:
135 explicit type_symbolt(const typet &_type)
136 {
137 type=_type;
138 is_type=true;
139 }
140};
141
147{
148public:
150 {
151 is_lvalue=true;
152 is_state_var=true;
153 is_thread_local=true;
154 is_file_local=true;
155 is_auxiliary=true;
156 }
157
160 {
161 this->name=name;
162 this->base_name=name;
163 this->type=type;
164 }
165};
166
171{
172public:
174 {
175 is_lvalue=true;
176 is_state_var=true;
177 is_thread_local=true;
178 is_file_local=true;
179 is_parameter=true;
180 }
181};
182
183#endif // CPROVER_UTIL_SYMBOL_H
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:158
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
Base class for all expressions.
Definition: expr.h:54
exprt()
Definition: expr.h:59
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:85
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
bool is_auxiliary
Definition: symbol.h:67
bool is_volatile
Definition: symbol.h:66
symbolt()
Definition: symbol.h:69
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool operator==(const symbolt &other) const
Definition: symbol.cpp:202
void show(std::ostream &out) const
Dump the state of a symbol object to a given output stream.
Definition: symbol.cpp:19
bool is_file_local
Definition: symbol.h:66
bool is_well_formed() const
Check that a symbol is well formed.
Definition: symbol.cpp:128
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:114
bool is_property
Definition: symbol.h:62
bool is_parameter
Definition: symbol.h:67
bool is_thread_local
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:107
bool is_state_var
Definition: symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
bool is_function() const
Definition: symbol.h:100
bool is_output
Definition: symbol.h:62
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:67
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:61
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool operator!=(const symbolt &other) const
Definition: symbol.cpp:233
bool is_shared() const
Definition: symbol.h:95
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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
bool is_input
Definition: symbol.h:62
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:133
type_symbolt(const typet &_type)
Definition: symbol.h:135
The type of an expression, extends irept.
Definition: type.h:29
dstringt irep_idt
Definition: irep.h:37
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:76