14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
44 for(
const auto ¶meter : code_type.
parameters())
95 body = std::move(other.body);
const parameterst & parameters() const
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_functiont & operator=(const goto_functiont &)=delete
std::vector< irep_idt > parameter_identifierst
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
void copy_from(const goto_functiont &other)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
goto_functiont(goto_functiont &&other)
bool body_available() const
void swap(goto_functiont &other)
goto_functiont(const goto_functiont &)=delete
goto_functiont & operator=(goto_functiont &&other)
void set_parameter_identifiers(const code_typet &code_type)
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
void swap(goto_programt &program)
Swap the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void get_local_identifiers(const goto_functiont &, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...