cprover
goto_functions_template.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H
16 
17 #include <ostream>
18 #include <cassert>
19 
20 #include <util/std_types.h>
21 #include <util/symbol.h>
22 #include <util/cprover_prefix.h>
23 
24 template <class bodyT>
26 {
27 public:
28  bodyT body;
30 
31  typedef std::vector<irep_idt> parameter_identifierst;
32  parameter_identifierst parameter_identifiers;
33 
34  bool body_available() const
35  {
36  return !body.instructions.empty();
37  }
38 
39  bool is_inlined() const
40  {
41  return type.get_bool(ID_C_inlined);
42  }
43 
44  bool is_hidden() const
45  {
46  return type.get_bool(ID_C_hide);
47  }
48 
49  void make_hidden()
50  {
51  type.set(ID_C_hide, true);
52  }
53 
55  {
56  }
57 
58  void clear()
59  {
60  body.clear();
61  type.clear();
62  parameter_identifiers.clear();
63  }
64 
66  {
67  body.swap(other.body);
68  type.swap(other.type);
69  parameter_identifiers.swap(other.parameter_identifiers);
70  }
71 
73  {
74  body.copy_from(other.body);
75  type=other.type;
76  parameter_identifiers=other.parameter_identifiers;
77  }
78 
81 
83  body(std::move(other.body)),
84  type(std::move(other.type)),
85  parameter_identifiers(std::move(other.parameter_identifiers))
86  {
87  }
88 
90  {
91  body=std::move(other.body);
92  type=std::move(other.type);
93  parameter_identifiers=std::move(other.parameter_identifiers);
94  return *this;
95  }
96 };
97 
98 template <class bodyT>
100 {
101 public:
103  typedef std::map<irep_idt, goto_functiont> function_mapt;
104  function_mapt function_map;
105 
107  {
108  }
109 
112 
114  function_map(std::move(other.function_map))
115  {
116  }
117 
119  {
120  function_map=std::move(other.function_map);
121  return *this;
122  }
123 
124  void clear()
125  {
126  function_map.clear();
127  }
128 
129  void output(
130  const namespacet &ns,
131  std::ostream &out) const;
132 
133  void compute_location_numbers();
134  void compute_loop_numbers();
135  void compute_target_numbers();
136  void compute_incoming_edges();
137 
138  void update()
139  {
140  compute_incoming_edges();
141  compute_target_numbers();
142  compute_location_numbers();
143  compute_loop_numbers();
144  }
145 
146  static inline irep_idt entry_point()
147  {
148  // do not confuse with C's "int main()"
149  return CPROVER_PREFIX "_start";
150  }
151 
153  {
154  function_map.swap(other.function_map);
155  }
156 
158  {
159  for(const auto &fun : other.function_map)
160  function_map[fun.first].copy_from(fun.second);
161  }
162 };
163 
164 template <class bodyT>
166  const namespacet &ns,
167  std::ostream &out) const
168 {
169  for(const auto &fun : function_map)
170  {
171  if(fun.second.body_available())
172  {
173  out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
174 
175  const symbolt &symbol=ns.lookup(fun.first);
176  out << symbol.display_name() << " /* " << symbol.name << " */\n";
177  fun.second.body.output(ns, symbol.name, out);
178 
179  out << std::flush;
180  }
181  }
182 }
183 
184 template <class bodyT>
186 {
187  unsigned nr=0;
188 
189  for(typename function_mapt::iterator
190  it=function_map.begin();
191  it!=function_map.end();
192  it++)
193  it->second.body.compute_location_numbers(nr);
194 }
195 
196 template <class bodyT>
198 {
199  for(typename function_mapt::iterator
200  it=function_map.begin();
201  it!=function_map.end();
202  it++)
203  it->second.body.compute_incoming_edges();
204 }
205 
206 template <class bodyT>
208 {
209  for(typename function_mapt::iterator
210  it=function_map.begin();
211  it!=function_map.end();
212  it++)
213  it->second.body.compute_target_numbers();
214 }
215 
216 template <class bodyT>
218 {
219  for(typename function_mapt::iterator
220  it=function_map.begin();
221  it!=function_map.end();
222  it++)
223  it->second.body.compute_loop_numbers();
224 }
225 
226 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H
std::map< irep_idt, goto_functiont > function_mapt
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Base type of functions.
Definition: std_types.h:734
Symbol table entry.
#define CPROVER_PREFIX
goto_function_templatet & operator=(goto_function_templatet &&other)
STL namespace.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void output(const namespacet &ns, std::ostream &out) const
parameter_identifierst parameter_identifiers
void copy_from(const goto_function_templatet &other)
void swap(goto_functions_templatet &other)
goto_function_templatet(goto_function_templatet &&other)
goto_functions_templatet(goto_functions_templatet &&other)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
goto_function_templatet< bodyT > goto_functiont
const irep_idt & display_name() const
Definition: symbol.h:60
API to type classes.
void swap(goto_function_templatet &other)
void copy_from(const goto_functions_templatet &other)
void clear()
Definition: irep.h:241
goto_function_templatet & operator=(const goto_function_templatet &)=delete
void swap(irept &irep)
Definition: irep.h:231
goto_functions_templatet & operator=(goto_functions_templatet &&other)
std::vector< irep_idt > parameter_identifierst
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214