cprover
cfg_infot Class Reference

Stores information about a goto function computed from its CFG, together with a target iterator into the instructions of the function. More...

#include <utils.h>

+ Collaboration diagram for cfg_infot:

Public Member Functions

 cfg_infot (const namespacet &_ns, goto_functiont &_goto_function)
 
void step ()
 Steps the target iterator forward. More...
 
bool is_not_local_or_dirty_local (irep_idt ident) const
 Returns true iff the given ident is either not a goto_function local or is a local that is dirty. More...
 
bool is_maybe_alive (const symbol_exprt &symbol_expr)
 Returns true whenever the given symbol_expr might be alive at the current target instruction. More...
 
bool is_local (irep_idt ident) const
 Returns true iff ident is a local (or parameter) of goto_function. More...
 
const goto_programt::targettget_current_target () const
 returns the current target instruction More...
 

Private Attributes

const namespacetns
 
goto_functiontgoto_function
 
goto_programt::targett target
 
const dirtyt dirty_analysis
 
const localst locals
 

Detailed Description

Stores information about a goto function computed from its CFG, together with a target iterator into the instructions of the function.

The methods of this class provide information about identifiers at the current target instruction to allow simplifying assigns clause checking assertions.

Definition at line 189 of file utils.h.

Constructor & Destructor Documentation

◆ cfg_infot()

cfg_infot::cfg_infot ( const namespacet _ns,
goto_functiont _goto_function 
)
inline

Definition at line 192 of file utils.h.

Member Function Documentation

◆ get_current_target()

const goto_programt::targett & cfg_infot::get_current_target ( ) const
inline

returns the current target instruction

Definition at line 234 of file utils.h.

◆ is_local()

bool cfg_infot::is_local ( irep_idt  ident) const
inline

Returns true iff ident is a local (or parameter) of goto_function.

Definition at line 227 of file utils.h.

◆ is_maybe_alive()

bool cfg_infot::is_maybe_alive ( const symbol_exprt symbol_expr)
inline

Returns true whenever the given symbol_expr might be alive at the current target instruction.

Definition at line 220 of file utils.h.

◆ is_not_local_or_dirty_local()

bool cfg_infot::is_not_local_or_dirty_local ( irep_idt  ident) const
inline

Returns true iff the given ident is either not a goto_function local or is a local that is dirty.

Definition at line 209 of file utils.h.

◆ step()

void cfg_infot::step ( )
inline

Steps the target iterator forward.

Definition at line 202 of file utils.h.

Member Data Documentation

◆ dirty_analysis

const dirtyt cfg_infot::dirty_analysis
private

Definition at line 243 of file utils.h.

◆ goto_function

goto_functiont& cfg_infot::goto_function
private

Definition at line 241 of file utils.h.

◆ locals

const localst cfg_infot::locals
private

Definition at line 244 of file utils.h.

◆ ns

const namespacet& cfg_infot::ns
private

Definition at line 240 of file utils.h.

◆ target

goto_programt::targett cfg_infot::target
private

Definition at line 242 of file utils.h.


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