CBMC
sese_regions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Single-entry, single-exit region analysis
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_SESE_REGIONS_H
13 #define CPROVER_ANALYSES_SESE_REGIONS_H
14 
16 {
17 public:
18  void operator()(const goto_programt &goto_program);
19  std::optional<goto_programt::const_targett>
21  {
22  auto find_result = sese_regions.find(entry);
23  if(find_result == sese_regions.end())
24  return {};
25  else
26  return find_result->second;
27  }
28 
29  void output(
30  std::ostream &out,
31  const goto_programt &goto_program,
32  const namespacet &ns) const;
33 
34 private:
35  std::unordered_map<
41  const goto_programt &goto_program,
42  const natural_loopst &natural_loops);
43 };
44 
45 #endif // CPROVER_ANALYSES_SESE_REGIONS_H
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:615
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Definition: natural_loops.h:88
std::optional< goto_programt::const_targett > get_region_exit(goto_programt::const_targett entry) const
Definition: sese_regions.h:20
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:39