13#ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
14#define CPROVER_ANALYSES_LOOP_ANALYSIS_H
33 template <
typename InstructionSet>
40 bool virtual contains(
const T instruction)
const
90 virtual void output(std::ostream &)
const;
112 template <
typename InstructionSet>
115 InstructionSet &&instructions)
124 const T instruction)
const
153 const T instruction)
const
172 for(
const auto &loop : loop_map)
174 unsigned n = loop.first->location_number;
176 std::unordered_set<std::size_t> backedge_location_numbers;
177 for(
const auto &backedge : loop.first->incoming_edges)
178 backedge_location_numbers.insert(backedge->location_number);
180 out << n <<
" is head of { ";
182 std::vector<std::size_t> loop_location_numbers;
183 for(
const auto &loop_instruction_it : loop.second)
184 loop_location_numbers.push_back(loop_instruction_it->location_number);
185 std::sort(loop_location_numbers.begin(), loop_location_numbers.end());
187 for(
const auto location_number : loop_location_numbers)
189 if(location_number != loop_location_numbers.at(0))
191 out << location_number;
192 if(backedge_location_numbers.count(location_number))
193 out <<
" (backedge)";
199template <
class LoopAnalysis>
204 out <<
"*** " << gf_entry.first <<
'\n';
206 LoopAnalysis loop_analysis;
207 loop_analysis(gf_entry.second.body);
208 loop_analysis.output(out);
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
linked_loop_analysist()=default
bool loop_contains(const typename loop_analysist< T >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
linked_loop_analysist & operator=(const linked_loop_analysist &)=delete
linked_loop_analysist(const linked_loop_analysist &)=delete
linked_loop_analysist(linked_loop_analysist &&)=delete
linked_loop_analysist & operator=(linked_loop_analysist &&)=delete
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
virtual void output(std::ostream &) const
Print all natural loops that were found.
loop_templatet< T > loopt
std::map< T, loopt > loop_mapt
A loop, specified as a set of instructions.
const_iterator end() const
Iterator over this loop's instructions.
std::set< T > loop_instructionst
loop_templatet(InstructionSet &&instructions)
bool empty() const
Returns true if this loop contains no instructions.
loop_instructionst loop_instructions
std::size_t size() const
Number of instructions in this loop.
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
loop_instructionst::const_iterator const_iterator
bool insert_instruction(const T instruction)
Adds instruction to this loop.
const_iterator begin() const
Iterator over this loop's instructions.
loop_analysist< T > parent_analysist
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis)
parent_analysist & loop_analysis
const parent_analysist & get_loop_analysis() const
Get the parent_analysist analysis this loop relates to.
bool loop_contains(const typename loop_analysist< T >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
parent_analysist & get_loop_analysis()
Get the parent_analysist analysis this loop relates to.
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis, InstructionSet &&instructions)
void show_loops(const goto_modelt &goto_model, std::ostream &out)