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.
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.
bool	is_maybe_alive (const symbol_exprt &symbol_expr)
	Returns true whenever the given symbol_expr might be alive at the current target instruction.
bool	is_local (irep_idt ident) const
	Returns true iff ident is a local (or parameter) of goto_function.
const goto_programt::targett &	get_current_target () const
	returns the current target instruction

Private Attributes
const namespacet &	ns
goto_functiont &	goto_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:

• goto-instrument/contracts/utils.h