14#ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
15#define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
37 return !
body.instructions.empty();
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=(goto_functiont &&other)
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
void set_parameter_identifiers(const code_typet &code_type)
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...
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...