Go to the documentation of this file.
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
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_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)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
void update_instructions_function(const irep_idt &function_id)
update the function member in each instruction
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 lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool get_bool(const irep_namet &name) const
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)
const std::string & id2string(const irep_idt &d)
goto_functiont & operator=(const goto_functiont &)=delete
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
A goto function, consisting of function type (see type), function body (see body),...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
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...
void clear()
Clear the goto program.
instructionst instructions
The list of instructions in the goto program.
goto_functiont & operator=(goto_functiont &&other)
std::unordered_set< irep_idt > find_symbols_sett
void set(const irep_namet &name, const irep_idt &value)
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.
code_typet type
The type of the function, indicating the return type and parameter types.
void swap(goto_programt &program)
Swap the goto program.