cprover
goto_functions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs with Functions
4
5Author: Daniel Kroening
6
7Date: 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{
26public:
28 typedef std::map<irep_idt, goto_functiont> function_mapt;
30
31private:
38
39public:
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
70 void unload(const irep_idt &name) { function_map.erase(name); }
71
72 void clear()
73 {
74 function_map.clear();
75 }
76
82
83 void update()
84 {
89 }
90
92 static inline irep_idt entry_point()
93 {
94 // do not confuse with C's "int main()"
95 return CPROVER_PREFIX "_start";
96 }
97
98 void swap(goto_functionst &other)
99 {
100 function_map.swap(other.function_map);
101 }
102
103 void copy_from(const goto_functionst &other)
104 {
105 for(const auto &fun : other.function_map)
106 function_map[fun.first].copy_from(fun.second);
107 }
108
109 std::vector<function_mapt::const_iterator> sorted() const;
110 std::vector<function_mapt::iterator> sorted();
111
116 void validate(const namespacet &, validation_modet) const;
117};
118
119#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.
goto_functionst & operator=(const goto_functionst &)=delete
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()
goto_functionst & operator=(goto_functionst &&other)
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
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:91
#define CPROVER_PREFIX
Goto Function.
STL namespace.
validation_modet