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
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_output
Definition: symbol.h:61
bool is_shared() const
Definition: symbol.h:95
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 of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:172
irep_idt mode
Language mode.
Definition: symbol.h:49
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
void set_compiled()
Set the symbol&#39;s value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:119
exprt()
Definition: expr.h:60
exprt value
Initial value of symbol.
Definition: symbol.h:34
type_symbolt(const typet &_type)
Definition: symbol.h:137
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
symbolt()
Definition: symbol.h:69
bool is_static_lifetime
Definition: symbol.h:65
bool is_input
Definition: symbol.h:61
Symbol table entry describing a data typeThis is a symbol generated as part of type checking...
Definition: symbol.h:134
const irep_idt & id() const
Definition: irep.h:259
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
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
bool is_compiled() const
Returns true iff the the symbol&#39;s value has been compiled to a goto program.
Definition: symbol.h:112
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:85
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:76
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:160
bool is_function() const
Definition: symbol.h:105
bool is_volatile
Definition: symbol.h:66
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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
Base class for all expressions.
Definition: expr.h:54
bool is_state_var
Definition: symbol.h:61
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
void make_nil()
Definition: irep.h:315
bool is_weak
Definition: symbol.h:66
bool is_procedure_local() const
Definition: symbol.h:100
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool is_auxiliary
Definition: symbol.h:66
dstringt irep_idt
Definition: irep.h:32
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