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>
124 const T instruction)
const
126 return loop.loop_instructions.count(instruction);
153 const T instruction)
const
155 return loop.loop_instructions.count(instruction);
172 for(
const auto &loop : loop_map)
174 unsigned n = loop.first->location_number;
177 for(
const auto &
backedge : loop.first->incoming_edges)
180 out <<
n <<
" is head of { ";
191 out << location_number;
193 out <<
" (backedge)";
199template <
class LoopAnalysis>
204 out <<
"*** " <<
gf_entry.first <<
'\n';
207 loop_analysis(
gf_entry.second.body);
208 loop_analysis.
output(out);
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...
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)