Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
107 std::vector<function_mapt::const_iterator>
sorted()
const;
108 std::vector<function_mapt::iterator>
sorted();
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++)
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++)
127 #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.
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
goto_functionst(const goto_functionst &)=delete
void compute_location_numbers()
function_mapt function_map
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void compute_target_numbers()
std::map< irep_idt, goto_functiont > function_mapt
goto_functionst(goto_functionst &&other)
A goto function, consisting of function type (see type), function body (see body),...
void compute_loop_numbers()
goto_functionst & operator=(const goto_functionst &)=delete
void unload(const irep_idt &name)
Remove function from the function map.
::goto_functiont goto_functiont
A collection of goto functions.
void copy_from(const goto_functionst &other)
void swap(goto_functionst &other)
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
void compute_incoming_edges()
goto_functionst & operator=(goto_functionst &&other)
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...