cprover
symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
27 class symbolt
28 {
29 public:
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();
78  value.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_hidden() const
122  {
123  return is_auxiliary;
124  }
125 
128  void set_hidden()
129  {
130  is_auxiliary = true;
131  }
132 
134  bool is_well_formed() const;
135 
136  bool operator==(const symbolt &other) const;
137  bool operator!=(const symbolt &other) const;
138 };
139 
140 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
141 
145 class type_symbolt:public symbolt
146 {
147 public:
148  explicit type_symbolt(const typet &_type)
149  {
150  type=_type;
151  is_type=true;
152  }
153 };
154 
160 {
161 public:
163  {
164  is_lvalue=true;
165  is_state_var=true;
166  is_thread_local=true;
167  is_file_local=true;
168  is_auxiliary=true;
169  }
170 
173  {
174  this->name=name;
175  this->base_name=name;
176  this->type=type;
177  }
178 };
179 
184 {
185 public:
187  {
188  is_lvalue=true;
189  is_state_var=true;
190  is_thread_local=true;
191  is_file_local=true;
192  is_parameter=true;
193  }
194 };
195 
196 #endif // CPROVER_UTIL_SYMBOL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:61
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
irept::make_nil
void make_nil()
Definition: irep.h:475
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbolt::operator==
bool operator==(const symbolt &other) const
Definition: symbol.cpp:203
symbolt::symbolt
symbolt()
Definition: symbol.h:69
symbolt::is_input
bool is_input
Definition: symbol.h:61
invariant.h
exprt::exprt
exprt()
Definition: expr.h:58
exprt
Base class for all expressions.
Definition: expr.h:52
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt
dstringt irep_idt
Definition: irep.h:32
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:159
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
operator<<
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:77
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
expr.h
symbolt::set_hidden
void set_hidden()
Mark a symbol for internal use.
Definition: symbol.h:128
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
symbolt::is_well_formed
bool is_well_formed() const
Check that a symbol is well formed.
Definition: symbol.cpp:129
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
symbolt::set_compiled
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
symbolt::is_function
bool is_function() const
Definition: symbol.h:100
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
auxiliary_symbolt::auxiliary_symbolt
auxiliary_symbolt()
Definition: symbol.h:162
type_symbolt::type_symbolt
type_symbolt(const typet &_type)
Definition: symbol.h:148
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:66
symbolt::is_shared
bool is_shared() const
Definition: symbol.h:95
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
source_locationt
Definition: source_location.h:19
symbolt::clear
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_output
bool is_output
Definition: symbol.h:61
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
symbolt::is_hidden
bool is_hidden() const
Returns true iff the symbol is marked for internal use.
Definition: symbol.h:121
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::show
void show(std::ostream &out) const
Dump the state of a symbol object to a given output stream.
Definition: symbol.cpp:20
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:66
symbolt::is_compiled
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:107
auxiliary_symbolt::auxiliary_symbolt
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:171
parameter_symbolt::parameter_symbolt
parameter_symbolt()
Definition: symbol.h:186
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
type_symbolt
Symbol table entry describing a data type.
Definition: symbol.h:145
symbolt::swap
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:86
symbolt::operator!=
bool operator!=(const symbolt &other) const
Definition: symbol.cpp:234
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
parameter_symbolt
Symbol table entry of function parameter.
Definition: symbol.h:183
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
symbolt::is_weak
bool is_weak
Definition: symbol.h:66
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:61