CBMC
Loading...
Searching...
No Matches
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:
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
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 {
80 }
81
87
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
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
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
goto_functionst & operator=(const goto_functionst &)=delete
void swap(goto_functionst &other)
std::map< irep_idt, goto_functiont > function_mapt
void compute_incoming_edges()
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()
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...
A generic container class for the GOTO intermediate representation of one function.
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