CBMC
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 
21 #include <map>
22 
25 {
26 public:
28  typedef std::map<irep_idt, goto_functiont> function_mapt;
30 
31 private:
38 
39 public:
42  {
43  }
44 
45  // Copying is unavailable as base class copy is deleted
46  // MSVC is unable to automatically determine this
49 
50  // Move operations need to be explicitly enabled as they are deleted with the
51  // copy operations
52  // default for move operations isn't available on Windows yet, so define
53  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
54  // under "Defaulted and Deleted Functions")
55 
57  function_map(std::move(other.function_map)),
59  {
60  }
61 
63  {
64  function_map=std::move(other.function_map);
65  unused_location_number=other.unused_location_number;
66  return *this;
67  }
68 
72  std::size_t unload(const irep_idt &name)
73  {
74  return function_map.erase(name);
75  }
76 
77  void clear()
78  {
79  function_map.clear();
80  }
81 
84  void compute_loop_numbers();
87 
88  void update()
89  {
94  }
95 
97  static inline irep_idt entry_point()
98  {
99  // do not confuse with C's "int main()"
100  return CPROVER_PREFIX "_start";
101  }
102 
103  void swap(goto_functionst &other)
104  {
105  function_map.swap(other.function_map);
106  }
107 
108  void copy_from(const goto_functionst &other)
109  {
110  for(const auto &fun : other.function_map)
111  function_map[fun.first].copy_from(fun.second);
112  }
113 
114  std::vector<function_mapt::const_iterator> sorted() const;
115  std::vector<function_mapt::iterator> sorted();
116 
121  void validate(const namespacet &, validation_modet) const;
122 };
123 
124 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
void swap(goto_functionst &other)
std::map< irep_idt, goto_functiont > function_mapt
void compute_incoming_edges()
void compute_loop_numbers()
std::size_t unload(const irep_idt &name)
Remove the function named name from the function map, if it exists.
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
::goto_functiont goto_functiont
void compute_location_numbers()
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
goto_functionst & operator=(const goto_functionst &)=delete
goto_functionst & operator=(goto_functionst &&other)
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
goto_functionst(goto_functionst &&other)
goto_functionst(const goto_functionst &)=delete
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void compute_target_numbers()
void copy_from(const goto_functionst &other)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
#define CPROVER_PREFIX
Goto Function.
validation_modet