cprover
Loading...
Searching...
No Matches
sese_regions.cpp File Reference

Single-entry, single-exit region analysis. More...

#include <sstream>
#include "cfg_dominators.h"
#include "natural_loops.h"
#include "sese_regions.h"
Include dependency graph for sese_regions.cpp:

Go to the source code of this file.

Typedefs

typedef std::unordered_map< goto_programt::const_targett, std::size_t, const_target_hashinnermost_loop_mapt
typedef std::unordered_map< goto_programt::const_targett, std::size_t, const_target_hashprogram_relative_instruction_indicest

Functions

static innermost_loop_mapt compute_innermost_loop_ids (const natural_loopst &natural_loops)
 Builds a map from instructions to the smallest (and therefore innermost) loop they are a member of.
static long get_innermost_loop (const innermost_loop_mapt &innermost_loops, const goto_programt::const_targett &target)
static std::string trimmed_last_line (const std::string &input)
static std::string instruction_ordinals (const goto_programt::const_targett &instruction, const program_relative_instruction_indicest &program_relative_instruction_indices)
static std::string brief_instruction_string (const goto_programt &goto_program, const goto_programt::const_targett &instruction, const namespacet &ns, const program_relative_instruction_indicest &program_relative_instruction_indices)

Detailed Description

Single-entry, single-exit region analysis.

Definition in file sese_regions.cpp.

Typedef Documentation

◆ innermost_loop_mapt

typedef std:: unordered_map<goto_programt::const_targett, std::size_t, const_target_hash> innermost_loop_mapt

Definition at line 76 of file sese_regions.cpp.

◆ program_relative_instruction_indicest

Definition at line 204 of file sese_regions.cpp.

Function Documentation

◆ brief_instruction_string()

std::string brief_instruction_string ( const goto_programt & goto_program,
const goto_programt::const_targett & instruction,
const namespacet & ns,
const program_relative_instruction_indicest & program_relative_instruction_indices )
static

Definition at line 216 of file sese_regions.cpp.

◆ compute_innermost_loop_ids()

innermost_loop_mapt compute_innermost_loop_ids ( const natural_loopst & natural_loops)
static

Builds a map from instructions to the smallest (and therefore innermost) loop they are a member of.

Definition at line 81 of file sese_regions.cpp.

◆ get_innermost_loop()

long get_innermost_loop ( const innermost_loop_mapt & innermost_loops,
const goto_programt::const_targett & target )
static

Definition at line 110 of file sese_regions.cpp.

◆ instruction_ordinals()

std::string instruction_ordinals ( const goto_programt::const_targett & instruction,
const program_relative_instruction_indicest & program_relative_instruction_indices )
static

Definition at line 206 of file sese_regions.cpp.

◆ trimmed_last_line()

std::string trimmed_last_line ( const std::string & input)
static

Definition at line 186 of file sese_regions.cpp.