cprover
symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
19 void 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";
30  if(is_thread_local)
31  out << " thread_local";
32  if(is_file_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 
76 std::ostream &operator<<(std::ostream &out,
77  const symbolt &symbol)
78 {
79  symbol.show(out);
80  return out;
81 }
82 
86 {
87  #define SYM_SWAP1(x) x.swap(b.x)
88 
89  SYM_SWAP1(type);
91  SYM_SWAP1(name);
95  SYM_SWAP1(mode);
97 
98  #define SYM_SWAP2(x) std::swap(x, b.x)
99 
116 }
117 
122 {
123  return symbol_exprt(name, type);
124 }
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.
141  {
142  return false;
143  }
144 
145  return true;
146 }
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_output
Definition: symbol.h:61
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:65
void show(std::ostream &out) const
Dump the state of a symbol object to a given output stream.
Definition: symbol.cpp:19
Symbol table entry.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
irep_idt mode
Language mode.
Definition: symbol.h:49
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
Symbol table entry.
Definition: symbol.h:27
bool is_static_lifetime
Definition: symbol.h:65
bool is_input
Definition: symbol.h:61
#define SYM_SWAP1(x)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
bool is_exported
Definition: symbol.h:61
bool is_parameter
Definition: symbol.h:66
API to expression classes.
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:76
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:85
bool is_volatile
Definition: symbol.h:66
bool is_extern
Definition: symbol.h:66
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_state_var
Definition: symbol.h:61
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
#define SYM_SWAP2(x)
bool is_file_local
Definition: symbol.h:66
bool is_weak
Definition: symbol.h:66
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool is_auxiliary
Definition: symbol.h:66
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
bool is_well_formed() const
Check that a symbol is well formed.
Definition: symbol.cpp:128
bool is_type
Definition: symbol.h:61
bool is_property
Definition: symbol.h:61
bool empty() const
Definition: dstring.h:75
bool is_macro
Definition: symbol.h:61
bool is_lvalue
Definition: symbol.h:66