CBMC
Loading...
Searching...
No Matches
symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "symbol.h"
10
11#include <ostream>
12
13#include "source_location.h"
14#include "std_expr.h"
15#include "suffix.h"
16
19void symbolt::show(std::ostream &out) const
20{
21 out << " " << name << '\n';
22 out << " type: " << type.pretty(4) << '\n'
23 << " value: " << value.pretty(4) << '\n';
24
25 out << " flags:";
26 if(is_lvalue)
27 out << " lvalue";
29 out << " static_lifetime";
31 out << " thread_local";
33 out << " file_local";
34 if(is_type)
35 out << " type";
36 if(is_extern)
37 out << " extern";
38 if(is_input)
39 out << " input";
40 if(is_output)
41 out << " output";
42 if(is_macro)
43 out << " macro";
44 if(is_parameter)
45 out << " parameter";
46 if(is_auxiliary)
47 out << " auxiliary";
48 if(is_weak)
49 out << " weak";
50 if(is_property)
51 out << " property";
52 if(is_state_var)
53 out << " state_var";
54 if(is_exported)
55 out << " exported";
56 if(is_volatile)
57 out << " volatile";
58 if(!mode.empty())
59 out << " mode=" << mode;
60 if(!base_name.empty())
61 out << " base_name=" << base_name;
62 if(!module.empty())
63 out << " module=" << module;
64 if(!pretty_name.empty())
65 out << " pretty_name=" << pretty_name;
66 out << '\n';
67 out << " location: " << location << '\n';
68
69 out << '\n';
70}
71
76std::ostream &operator<<(std::ostream &out,
77 const symbolt &symbol)
78{
79 symbol.show(out);
80 return out;
81}
82
117
125
129{
130 // Well-formedness criterion number 1 is for a symbol
131 // to have a non-empty mode (see #1880)
132 if(mode.empty())
133 {
134 return false;
135 }
136
137 // Well-formedness criterion number 2 is for a symbol
138 // to have it's base name as a suffix to it's more
139 // general name.
140
141 // Exception: Java symbols' base names do not have type signatures
142 // (for example, they can have name "someclass.method:(II)V" and base name
143 // "method")
144 if(
146 mode != ID_cpp)
147 {
148 bool criterion_must_hold = true;
149
150 // There are some special cases where this criterion doesn't hold, check
151 // to see if we have one of those cases
152
153 if(is_type)
154 {
155 // Typedefs
156 if(
157 type.find(ID_C_typedef).is_not_nil() &&
159 {
160 criterion_must_hold = false;
161 }
162
163 // Tag types
164 if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
165 {
166 criterion_must_hold = false;
167 }
168 }
169
170 // Linker renaming may have added $linkN suffixes to the name, and other
171 // suffixes such as #return_value may have then be subsequently added.
172 // Strip out the first $linkN substring and then see if the criterion holds
173 const auto &unstripped_name = id2string(name);
174 const size_t dollar_link_start_pos = unstripped_name.find("$link");
175
176 if(dollar_link_start_pos != std::string::npos)
177 {
180 {
182 }
183
184 const auto stripped_name =
186 unstripped_name.substr(dollar_link_end_pos, std::string::npos);
187
189 criterion_must_hold = false;
190 }
191
193 {
194 // For all other cases this criterion should hold
195 return false;
196 }
197 }
198
199 return true;
200}
201
202bool symbolt::operator==(const symbolt &other) const
203{
204 // clang-format off
205 return
206 type == other.type &&
207 value == other.value &&
208 location == other.location &&
209 name == other.name &&
210 module == other.module &&
211 base_name == other.base_name &&
212 mode == other.mode &&
213 pretty_name == other.pretty_name &&
214 is_type == other.is_type &&
215 is_macro == other.is_macro &&
216 is_exported == other.is_exported &&
217 is_input == other.is_input &&
218 is_output == other.is_output &&
219 is_state_var == other.is_state_var &&
220 is_property == other.is_property &&
221 is_parameter == other.is_parameter &&
222 is_auxiliary == other.is_auxiliary &&
223 is_weak == other.is_weak &&
224 is_lvalue == other.is_lvalue &&
225 is_static_lifetime == other.is_static_lifetime &&
226 is_thread_local == other.is_thread_local &&
227 is_file_local == other.is_file_local &&
228 is_extern == other.is_extern &&
229 is_volatile == other.is_volatile;
230 // clang-format on
231}
232
233bool symbolt::operator!=(const symbolt &other) const
234{
235 return !(*this == other);
236}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
bool empty() const
Definition dstring.h:89
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
Expression to hold a symbol (variable)
Definition std_expr.h:131
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition std_expr.h:166
Symbol table entry.
Definition symbol.h:28
void swap(symbolt &b)
Swap values between two symbols.
Definition symbol.cpp:85
bool is_auxiliary
Definition symbol.h:77
bool is_volatile
Definition symbol.h:75
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
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:73
bool is_well_formed() const
Check that a symbol is well formed.
Definition symbol.cpp:128
bool is_static_lifetime
Definition symbol.h:70
bool is_property
Definition symbol.h:67
bool is_parameter
Definition symbol.h:76
bool is_thread_local
Definition symbol.h:71
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
bool is_state_var
Definition symbol.h:66
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
bool is_output
Definition symbol.h:65
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:78
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_exported
Definition symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
bool operator!=(const symbolt &other) const
Definition symbol.cpp:233
bool is_lvalue
Definition symbol.h:72
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:64
int isdigit(int c)
Definition ctype.c:24
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
#define SYM_SWAP2(x)
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition symbol.cpp:76
#define SYM_SWAP1(x)
Symbol table entry.