Go to the documentation of this file.
20 std::set<irep_idt> &dest)
27 if(!identifier.empty())
28 dest.insert(identifier);
45 "last instruction should be of end function type");
53 for(
const auto &identifier : typetags)
56 vm, !ns.
lookup(identifier, symbol),
id2string(identifier) +
" not found");
66 !instruction->is_return(),
67 "void function should not return a value");
#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 get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
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 body_available() const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const std::string & id2string(const irep_idt &d)
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 get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
instructionst instructions
The list of instructions in the goto program.
std::unordered_set< irep_idt > find_symbols_sett
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.
#define forall_goto_program_instructions(it, program)