21 natural_loops(goto_program);
44 predecessor->location_number > it->location_number &&
54 for(
const auto &loop : natural_loops.
loop_map)
57 loop.first->incoming_edges.begin(),
58 loop.first->incoming_edges.end(),
60 return loop.first->location_number < predecessor->location_number;
75 unordered_map<goto_programt::const_targett, std::size_t, const_target_hash>
86 std::size_t loop_id = 0;
92 for(
const auto &instruction : loop)
118 return (
long)
findit->second;
139 successors.size() == 1 &&
140 (*successors.begin())->incoming_edges.size() == 1)
181 emplace_result.second,
"should only visit each region entry once");
203 unordered_map<goto_programt::const_targett, std::size_t, const_target_hash>
213 ", " + std::to_string(instruction->location_number) +
")";
223 std::ostringstream
ostr;
244 <<
" single-entry, single-exit regions:\n";
247 out <<
"Region starting at "
Compute dominators for CFG of goto_function.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
void operator()(const goto_programt &goto_program)
void compute_sese_regions(const goto_programt &goto_program, const natural_loopst &natural_loops)
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
std::unordered_map< goto_programt::const_targett, goto_programt::const_targett, const_target_hash > sese_regions
Compute natural loops in a goto_function.
static std::string instruction_ordinals(const goto_programt::const_targett &instruction, const program_relative_instruction_indicest &program_relative_instruction_indices)
static long get_innermost_loop(const innermost_loop_mapt &innermost_loops, const goto_programt::const_targett &target)
std::unordered_map< goto_programt::const_targett, std::size_t, const_target_hash > innermost_loop_mapt
static std::string brief_instruction_string(const goto_programt &goto_program, const goto_programt::const_targett &instruction, const namespacet &ns, const program_relative_instruction_indicest &program_relative_instruction_indices)
static innermost_loop_mapt compute_innermost_loop_ids(const natural_loopst &natural_loops)
Builds a map from instructions to the smallest (and therefore innermost) loop they are a member of.
static std::string trimmed_last_line(const std::string &input)
std::unordered_map< goto_programt::const_targett, std::size_t, const_target_hash > program_relative_instruction_indicest
Single-entry, single-exit region analysis.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.