CBMC
Public Member Functions | Private Member Functions | Private Attributes | List of all members
sese_region_analysist Class Reference

#include <sese_regions.h>

+ Collaboration diagram for sese_region_analysist:

Public Member Functions

void operator() (const goto_programt &goto_program)
 
std::optional< goto_programt::const_targett > get_region_exit (goto_programt::const_targett entry) const
 
void output (std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
 

Private Member Functions

void compute_sese_regions (const goto_programt &goto_program, const natural_loopst &natural_loops)
 

Private Attributes

std::unordered_map< goto_programt::const_targett, goto_programt::const_targett, const_target_hash > sese_regions
 

Detailed Description

Definition at line 15 of file sese_regions.h.

Member Function Documentation

◆ compute_sese_regions()

void sese_region_analysist::compute_sese_regions ( const goto_programt &  goto_program,
const natural_loopst &  natural_loops 
)
private

Definition at line 121 of file sese_regions.cpp.

◆ get_region_exit()

std::optional<goto_programt::const_targett> sese_region_analysist::get_region_exit ( goto_programt::const_targett  entry) const
inline

Definition at line 20 of file sese_regions.h.

◆ operator()()

void sese_region_analysist::operator() ( const goto_programt &  goto_program)

Definition at line 18 of file sese_regions.cpp.

◆ output()

void sese_region_analysist::output ( std::ostream &  out,
const goto_programt &  goto_program,
const namespacet &  ns 
) const

Definition at line 230 of file sese_regions.cpp.

Member Data Documentation

◆ sese_regions

std::unordered_map< goto_programt::const_targett, goto_programt::const_targett, const_target_hash> sese_region_analysist::sese_regions
private

Definition at line 39 of file sese_regions.h.

The documentation for this class was generated from the following files: