14#ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
15#define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
109 std::vector<function_mapt::const_iterator>
sorted()
const;
110 std::vector<function_mapt::iterator>
sorted();
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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...
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...