Go to the documentation of this file.
40 func.second.body.compute_incoming_edges();
48 func.second.body.compute_target_numbers();
56 func.second.body.compute_loop_numbers();
61 std::vector<goto_functionst::function_mapt::const_iterator>
64 std::vector<function_mapt::const_iterator> result;
74 [](function_mapt::const_iterator a, function_mapt::const_iterator b) {
75 return id2string(a->first) < id2string(b->first);
84 std::vector<function_mapt::iterator> result;
94 [](function_mapt::iterator a, function_mapt::iterator b) {
95 return id2string(a->first) < id2string(b->first);
107 const auto &function_name = entry.first;
114 goto_function.
type == ns.
lookup(function_name).type,
115 id2string(function_name) +
" type inconsistency\ngoto program type: " +
117 "\nsymbol table type: " + ns.
lookup(function_name).type.id_string());
122 id2string(function_name) +
" parameter count inconsistency\n" +
128 for(
const auto ¶meter : parameters)
132 it->empty() || ns.
lookup(*it).type == parameter.type(),
133 id2string(function_name) +
" parameter type inconsistency\n" +
134 "goto program: " + ns.
lookup(*it).type.id_string() +
135 "\nsymbol table: " + parameter.type().id_string());
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
std::vector< parametert > parameterst
typet type
Type of symbol.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
void compute_location_numbers()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
function_mapt function_map
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().
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void compute_target_numbers()
const std::string & id2string(const irep_idt &d)
void compute_location_numbers(unsigned &nr)
Compute location numbers.
const std::string & id_string() const
A goto function, consisting of function type (see type), function body (see body),...
void compute_loop_numbers()
const parameterst & parameters() const
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
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.
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
void compute_incoming_edges()
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...