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 
23 {
24 public:
26  typedef std::map<irep_idt, goto_functiont> function_mapt;
28 
29 private:
36 
37 public:
40  {
41  }
42 
43  // Copying is unavailable as base class copy is deleted
44  // MSVC is unable to automatically determine this
47 
48  // Move operations need to be explicitly enabled as they are deleted with the
49  // copy operations
50  // default for move operations isn't available on Windows yet, so define
51  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
52  // under "Defaulted and Deleted Functions")
53 
55  function_map(std::move(other.function_map)),
57  {
58  }
59 
61  {
62  function_map=std::move(other.function_map);
63  unused_location_number=other.unused_location_number;
64  return *this;
65  }
66 
68  void unload(const irep_idt &name) { function_map.erase(name); }
69 
70  void clear()
71  {
72  function_map.clear();
73  }
74 
77  void compute_loop_numbers();
80 
81  void update()
82  {
87  }
88 
90  static inline irep_idt entry_point()
91  {
92  // do not confuse with C's "int main()"
93  return CPROVER_PREFIX "_start";
94  }
95 
96  void swap(goto_functionst &other)
97  {
98  function_map.swap(other.function_map);
99  }
100 
101  void copy_from(const goto_functionst &other)
102  {
103  for(const auto &fun : other.function_map)
104  function_map[fun.first].copy_from(fun.second);
105  }
106 
107  std::vector<function_mapt::const_iterator> sorted() const;
108  std::vector<function_mapt::iterator> sorted();
109 
114  void validate(const namespacet &, validation_modet) const;
115 };
116 
117 #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:37
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()
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
void unload(const irep_idt &name)
Remove function from the function map.
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:27
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
#define CPROVER_PREFIX
Goto Function.
validation_modet