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_procedure_local() const
101  {
102  return !is_static_lifetime;
103  }
104 
105  bool is_function() const
106  {
107  return !is_type && !is_macro && type.id()==ID_code;
108  }
109 
112  bool is_compiled() const
113  {
114  return type.id() == ID_code && value == exprt(ID_compiled);
115  }
116 
120  {
121  PRECONDITION(type.id() == ID_code);
122  value = exprt(ID_compiled);
123  }
124 
126  bool is_well_formed() const;
127 };
128 
129 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
130 
134 class type_symbolt:public symbolt
135 {
136 public:
137  explicit type_symbolt(const typet &_type)
138  {
139  type=_type;
140  is_type=true;
141  }
142 };
143 
149 {
150 public:
152  {
153  is_lvalue=true;
154  is_state_var=true;
155  is_thread_local=true;
156  is_file_local=true;
157  is_auxiliary=true;
158  }
159 
162  {
163  this->name=name;
164  this->base_name=name;
165  this->type=type;
166  }
167 };
168 
173 {
174 public:
176  {
177  is_lvalue=true;
178  is_state_var=true;
179  is_thread_local=true;
180  is_file_local=true;
181  is_parameter=true;
182  }
183 };
184 
185 #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:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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:315
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:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbolt::symbolt
symbolt()
Definition: symbol.h:69
symbolt::is_input
bool is_input
Definition: symbol.h:61
exprt::exprt
exprt()
Definition: expr.h:60
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
invariant.h
irep_idt
dstringt irep_idt
Definition: irep.h:32
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:148
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
operator<<
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:76
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
expr.h
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:128
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:119
symbolt::is_function
bool is_function() const
Definition: symbol.h:105
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
auxiliary_symbolt::auxiliary_symbolt
auxiliary_symbolt()
Definition: symbol.h:151
type_symbolt::type_symbolt
type_symbolt(const typet &_type)
Definition: symbol.h:137
symbolt::is_procedure_local
bool is_procedure_local() const
Definition: symbol.h:100
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:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
source_locationt
Definition: source_location.h:20
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_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:19
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:112
auxiliary_symbolt::auxiliary_symbolt
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:160
parameter_symbolt::parameter_symbolt
parameter_symbolt()
Definition: symbol.h:175
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
type_symbolt
Symbol table entry describing a data type.
Definition: symbol.h:134
symbolt::swap
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:85
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:172
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