13 #ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
14 #define CPROVER_ANALYSES_LOOP_ANALYSIS_H
18 template <
class T,
typename C>
22 template <
class T,
typename C>
33 template <
typename InstructionSet>
40 bool virtual contains(
const T instruction)
const
80 template <
class T,
typename C>
90 virtual void output(std::ostream &)
const;
101 template <
typename T,
typename C>
112 template <
typename InstructionSet>
115 InstructionSet &&instructions)
116 :
loop_templatet<T, C>(std::forward<InstructionSet>(instructions)),
124 const T instruction)
const
144 template <
class T,
typename C>
153 const T instruction)
const
169 template <
class T,
typename C>
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)";
199 template <
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.
bool loop_contains(const typename loop_analysist< T, C >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
linked_loop_analysist & operator=(linked_loop_analysist &&)=delete
linked_loop_analysist(const linked_loop_analysist &)=delete
linked_loop_analysist(linked_loop_analysist &&)=delete
linked_loop_analysist & operator=(const linked_loop_analysist &)=delete
linked_loop_analysist()=default
std::map< T, loopt, C > loop_mapt
loop_templatet< T, C > loopt
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.
A loop, specified as a set of instructions.
loop_instructionst loop_instructions
bool insert_instruction(const T instruction)
Adds instruction to this loop.
const_iterator end() const
Iterator over this loop's instructions.
const_iterator begin() const
Iterator over this loop's instructions.
std::size_t size() const
Number of instructions in this loop.
bool empty() const
Returns true if this loop contains no instructions.
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
loop_templatet(InstructionSet &&instructions)
loop_instructionst::const_iterator const_iterator
std::set< T, C > loop_instructionst
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis, InstructionSet &&instructions)
bool loop_contains(const typename loop_analysist< T, C >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis)
parent_analysist & get_loop_analysis()
Get the parent_analysist analysis this loop relates to.
const parent_analysist & get_loop_analysis() const
Get the parent_analysist analysis this loop relates to.
parent_analysist & loop_analysis
loop_analysist< T, C > parent_analysist
void show_loops(const goto_modelt &goto_model, std::ostream &out)