Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
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...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void compute_target_numbers()
void update_instructions_function()
update the function member in each instruction by setting it to the goto function's identifier
std::map< irep_idt, goto_functiont > function_mapt
const std::string & id2string(const irep_idt &d)
goto_functionst(goto_functionst &&other)
const std::string & id_string() const
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 validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
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.
code_typet type
The type of the function, indicating the return type and parameter types.
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...