14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H 15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H 87 func.second.update_instructions_function(func.first);
118 std::vector<function_mapt::const_iterator>
sorted()
const;
119 std::vector<function_mapt::iterator>
sorted();
130 const auto &function_name = entry.first;
134 goto_function.
type == ns.
lookup(function_name).type,
135 id2string(function_name) +
" type inconsistency\ngoto program type: " +
137 "\nsymbol table type: " + ns.
lookup(function_name).type.id_string());
144 #define Forall_goto_functions(it, functions) \ 145 for(goto_functionst::function_mapt::iterator \ 146 it=(functions).function_map.begin(); \ 147 it!=(functions).function_map.end(); it++) 149 #define forall_goto_functions(it, functions) \ 150 for(goto_functionst::function_mapt::const_iterator \ 151 it=(functions).function_map.begin(); \ 152 it!=(functions).function_map.end(); it++) 154 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H const std::string & id2string(const irep_idt &d)
goto_functionst(goto_functionst &&other)
void copy_from(const goto_functionst &other)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
void compute_loop_numbers()
void compute_target_numbers()
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
function_mapt function_map
goto_functionst & operator=(goto_functionst &&other)
void compute_location_numbers()
void update_instructions_function()
update the function member in each instruction by setting it to the goto function's identifier ...
void swap(goto_functionst &other)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
A collection of goto functions.
std::map< irep_idt, goto_functiont > function_mapt
code_typet type
The type of the function, indicating the return type and parameter types.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
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 unload(const irep_idt &name)
Remove function from the function map.
const std::string & id_string() const
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
goto_functionst & operator=(const goto_functionst &)=delete
void compute_incoming_edges()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().