cprover
sese_regions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Single-entry, single-exit region analysis
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_SESE_REGIONS_H
13#define CPROVER_ANALYSES_SESE_REGIONS_H
14
17#include <util/optional.h>
18
20{
21public:
22 void operator()(const goto_programt &goto_program);
25 {
26 auto find_result = sese_regions.find(entry);
27 if(find_result == sese_regions.end())
28 return {};
29 else
30 return find_result->second;
31 }
32
33 void output(
34 std::ostream &out,
35 const goto_programt &goto_program,
36 const namespacet &ns) const;
37
38private:
39 std::unordered_map<
45 const goto_programt &goto_program,
46 const natural_loopst &natural_loops);
47};
48
49#endif // CPROVER_ANALYSES_SESE_REGIONS_H
Compute dominators for CFG of goto_function.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Definition: natural_loops.h:86
optionalt< goto_programt::const_targett > get_region_exit(goto_programt::const_targett entry) const
Definition: sese_regions.h:24
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
Definition: sese_regions.h:43
Compute natural loops in a goto_function.
nonstd::optional< T > optionalt
Definition: optional.h:35