Go to the documentation of this file.
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);
113 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
goto_functiont(goto_functiont &&other)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool body_available() const
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...
void swap(goto_functiont &other)
goto_functiont & operator=(const goto_functiont &)=delete
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
const parameterst & parameters() const
void set_parameter_identifiers(const code_typet &code_type)
void clear()
Clear the goto program.
instructionst instructions
The list of instructions in the goto program.
goto_functiont & operator=(goto_functiont &&other)
void copy_from(const goto_functiont &other)
A generic container class for the GOTO intermediate representation of one function.
std::vector< irep_idt > parameter_identifierst
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
void swap(goto_programt &program)
Swap the goto program.