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 #define Forall_goto_functions(it, functions) \
118  for(goto_functionst::function_mapt::iterator \
119  it=(functions).function_map.begin(); \
120  it!=(functions).function_map.end(); it++)
121 
122 #define forall_goto_functions(it, functions) \
123  for(goto_functionst::function_mapt::const_iterator \
124  it=(functions).function_map.begin(); \
125  it!=(functions).function_map.end(); it++)
126 
127 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functionst::validate
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
Definition: goto_functions.cpp:101
goto_functionst::goto_functionst
goto_functionst(const goto_functionst &)=delete
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_functionst::clear
void clear()
Definition: goto_functions.h:70
goto_functionst::compute_target_numbers
void compute_target_numbers()
Definition: goto_functions.cpp:44
goto_functionst::function_mapt
std::map< irep_idt, goto_functiont > function_mapt
Definition: goto_functions.h:26
goto_functionst::goto_functionst
goto_functionst(goto_functionst &&other)
Definition: goto_functions.h:54
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
cprover_prefix.h
goto_functionst::operator=
goto_functionst & operator=(const goto_functionst &)=delete
goto_functionst::unload
void unload(const irep_idt &name)
Remove function from the function map.
Definition: goto_functions.h:68
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_functionst::goto_functionst
goto_functionst()
Definition: goto_functions.h:38
goto_functionst::copy_from
void copy_from(const goto_functionst &other)
Definition: goto_functions.h:101
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
goto_functionst::swap
void swap(goto_functionst &other)
Definition: goto_functions.h:96
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
goto_function.h
Goto Function.
goto_functionst::compute_incoming_edges
void compute_incoming_edges()
Definition: goto_functions.cpp:36
goto_functionst::operator=
goto_functionst & operator=(goto_functionst &&other)
Definition: goto_functions.h:60
goto_functionst::unused_location_number
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
Definition: goto_functions.h:35