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 
23 #include <iosfwd>
24 
25 #include "expr.h"
26 
33 class symbolt
34 {
35 public:
38 
41 
44 
47 
50 
53 
56 
59 
60  const irep_idt &display_name() const
61  {
62  return pretty_name.empty()?name:pretty_name;
63  }
64 
65  // global use
68 
69  // ANSI-C
73 
75  {
76  clear();
77  }
78 
79  void clear()
80  {
81  type.make_nil();
82  value.make_nil();
83  location.make_nil();
84 
85  name=module=base_name=mode=pretty_name=irep_idt();
86 
87  is_type=is_macro=is_exported=
88  is_input=is_output=is_state_var=is_property=
89  is_static_lifetime=is_thread_local=
90  is_lvalue=is_file_local=is_extern=is_volatile=
91  is_parameter=is_auxiliary=is_weak=false;
92  }
93 
94  void swap(symbolt &b);
95  void show(std::ostream &out) const;
96 
97  // serialization
98  irept to_irep() const;
99  void from_irep(const irept &src);
100 
101  class symbol_exprt symbol_expr() const;
102 
103  bool is_shared() const
104  {
105  return !is_thread_local;
106  }
107 
108  bool is_procedure_local() const
109  {
110  return !is_static_lifetime;
111  }
112 };
113 
114 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
115 
121 class type_symbolt:public symbolt
122 {
123 public:
124  explicit type_symbolt(const typet &_type)
125  {
126  type=_type;
127  is_type=true;
128  }
129 };
130 
138 {
139 public:
141  {
142  is_lvalue=true;
143  is_state_var=true;
144  is_thread_local=true;
145  is_file_local=true;
146  is_auxiliary=true;
147  }
148 
151  {
152  this->name=name;
153  this->base_name=name;
154  this->type=type;
155  }
156 };
157 
164 {
165 public:
167  {
168  is_lvalue=true;
169  is_state_var=true;
170  is_thread_local=true;
171  is_file_local=true;
172  is_parameter=true;
173  }
174 };
175 
176 #endif // CPROVER_UTIL_SYMBOL_H
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
bool is_output
Definition: symbol.h:66
bool is_shared() const
Definition: symbol.h:103
bool is_thread_local
Definition: symbol.h:70
void show(std::ostream &out) const
Definition: symbol.cpp:16
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:163
irep_idt mode
Language mode.
Definition: symbol.h:55
void clear()
Definition: symbol.h:79
exprt value
Initial value of symbol.
Definition: symbol.h:40
type_symbolt(const typet &_type)
Definition: symbol.h:124
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symbolt()
Definition: symbol.h:74
bool is_static_lifetime
Definition: symbol.h:70
bool is_input
Definition: symbol.h:66
Symbol table entry describing a data typeThis is a symbol generated as part of type checking...
Definition: symbol.h:121
bool is_exported
Definition: symbol.h:66
bool is_parameter
Definition: symbol.h:71
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
Base class for tree-like data structures with sharing.
Definition: irep.h:87
void swap(symbolt &b)
Definition: symbol.cpp:156
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Definition: symbol.cpp:69
auxiliary_symbolt(const irep_idt &name, const typet &type)
Definition: symbol.h:149
bool is_volatile
Definition: symbol.h:71
const irep_idt & display_name() const
Definition: symbol.h:60
bool is_extern
Definition: symbol.h:71
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
Base class for all expressions.
Definition: expr.h:46
bool is_state_var
Definition: symbol.h:66
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
bool is_file_local
Definition: symbol.h:71
void make_nil()
Definition: irep.h:243
bool is_weak
Definition: symbol.h:71
void from_irep(const irept &src)
Definition: symbol.cpp:126
bool is_procedure_local() const
Definition: symbol.h:108
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool is_auxiliary
Definition: symbol.h:71
dstringt irep_idt
Definition: irep.h:32
bool is_type
Definition: symbol.h:66
bool is_property
Definition: symbol.h:66
irept to_irep() const
Definition: symbol.cpp:76
bool empty() const
Definition: dstring.h:61
bool is_macro
Definition: symbol.h:66
bool is_lvalue
Definition: symbol.h:71