14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H 15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H 109 body = std::move(other.body);
110 type = std::move(other.type);
126 for(
const auto &identifier : typetags)
130 !ns.
lookup(identifier, symbol),
140 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
const std::string & id2string(const irep_idt &d)
void swap(goto_functiont &other)
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes) ...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
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.
bool get_bool(const irep_namet &name) const
std::vector< irep_idt > parameter_identifierst
void update_instructions_function(const irep_idt &function_id)
update the function member in each instruction
goto_functiont & operator=(const goto_functiont &)=delete
void clear()
Clear the goto program.
goto_functiont(goto_functiont &&other)
instructionst instructions
The list of instructions in the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
void copy_from(const goto_functiont &other)
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...
goto_functiont & operator=(goto_functiont &&other)
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
void swap(goto_programt &program)
Swap the goto program.
A generic container class for the GOTO intermediate representation of one function.
bool body_available() const
void update_instructions_function(const irep_idt &function_id)
Sets the function member of each instruction if not yet set Note that a goto program need not be a go...
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
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...
std::unordered_set< irep_idt > find_symbols_sett
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)