cprover
goto_functions.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_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
16 
17 #include "goto_function.h"
18 
19 #include <util/cprover_prefix.h>
20 
22 {
23 public:
25  typedef std::map<irep_idt, goto_functiont> function_mapt;
27 
28 private:
35 
36 public:
39  {
40  }
41 
42  // Copying is unavailable as base class copy is deleted
43  // MSVC is unable to automatically determine this
44  goto_functionst(const goto_functionst &)=delete;
45  goto_functionst &operator=(const goto_functionst &)=delete;
46 
47  // Move operations need to be explicitly enabled as they are deleted with the
48  // copy operations
49  // default for move operations isn't available on Windows yet, so define
50  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
51  // under "Defaulted and Deleted Functions")
52 
54  function_map(std::move(other.function_map)),
56  {
57  }
58 
60  {
61  function_map=std::move(other.function_map);
62  unused_location_number=other.unused_location_number;
63  return *this;
64  }
65 
66  void unload(const irep_idt &name) { function_map.erase(name); }
67 
68  void clear()
69  {
70  function_map.clear();
71  }
72 
73  void output(
74  const namespacet &ns,
75  std::ostream &out) const;
76 
79  void compute_loop_numbers();
82 
86  {
87  for(auto &func : function_map)
88  {
89  func.second.update_instructions_function(func.first);
90  }
91  }
92 
93  void update()
94  {
100  }
101 
102  static inline irep_idt entry_point()
103  {
104  // do not confuse with C's "int main()"
105  return CPROVER_PREFIX "_start";
106  }
107 
108  void swap(goto_functionst &other)
109  {
110  function_map.swap(other.function_map);
111  }
112 
113  void copy_from(const goto_functionst &other)
114  {
115  for(const auto &fun : other.function_map)
116  function_map[fun.first].copy_from(fun.second);
117  }
118 };
119 
120 #define Forall_goto_functions(it, functions) \
121  for(goto_functionst::function_mapt::iterator \
122  it=(functions).function_map.begin(); \
123  it!=(functions).function_map.end(); it++)
124 
125 #define forall_goto_functions(it, functions) \
126  for(goto_functionst::function_mapt::const_iterator \
127  it=(functions).function_map.begin(); \
128  it!=(functions).function_map.end(); it++)
129 
130 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
goto_functionst(goto_functionst &&other)
#define CPROVER_PREFIX
void copy_from(const goto_functionst &other)
void compute_loop_numbers()
void compute_target_numbers()
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
function_mapt function_map
STL namespace.
goto_functionst & operator=(goto_functionst &&other)
void compute_location_numbers()
void update_instructions_function()
update the function member in each instruction by setting it to the goto function&#39;s identifier ...
void swap(goto_functionst &other)
void output(const namespacet &ns, std::ostream &out) const
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
std::map< irep_idt, goto_functiont > function_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
static irep_idt entry_point()
void unload(const irep_idt &name)
goto_functionst & operator=(const goto_functionst &)=delete
void compute_incoming_edges()