flow_insensitive_abstract_domain_baset Class Reference

#include <flow_insensitive_analysis.h>

Inheritance diagram for flow_insensitive_abstract_domain_baset:

Public Types
typedef goto_programt::const_targett	locationt
typedef std::unordered_set< exprt, irep_hash >	expr_sett

Public Member Functions
	flow_insensitive_abstract_domain_baset ()
virtual void	initialize (const namespacet &ns)=0
virtual bool	transform (const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
virtual	~flow_insensitive_abstract_domain_baset ()
virtual void	output (const namespacet &, std::ostream &) const
virtual void	get_reference_set (const namespacet &, const exprt &, expr_sett &expr_set)
virtual void	clear (void)=0

Protected Member Functions
exprt	get_guard (locationt from, locationt to) const
exprt	get_return_lhs (locationt to) const

Protected Attributes
bool	changed

Detailed Description

Definition at line 36 of file flow_insensitive_analysis.h.

Member Typedef Documentation

expr_sett

typedef std::unordered_set<exprt, irep_hash> flow_insensitive_abstract_domain_baset::expr_sett

Definition at line 65 of file flow_insensitive_analysis.h.

locationt

typedef goto_programt::const_targett flow_insensitive_abstract_domain_baset::locationt

Definition at line 44 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

flow_insensitive_abstract_domain_baset()

flow_insensitive_abstract_domain_baset::flow_insensitive_abstract_domain_baset ( )

inline

Definition at line 39 of file flow_insensitive_analysis.h.

~flow_insensitive_abstract_domain_baset()

virtual flow_insensitive_abstract_domain_baset::~flow_insensitive_abstract_domain_baset ( )

inlinevirtual

Definition at line 55 of file flow_insensitive_analysis.h.

Member Function Documentation

clear()

virtual void flow_insensitive_abstract_domain_baset::clear ( void  )

pure virtual

Implemented in value_set_domain_fit.

get_guard()

exprt flow_insensitive_abstract_domain_baset::get_guard ( locationt  from, locationt  to  ) const

protected

Definition at line 19 of file flow_insensitive_analysis.cpp.

get_reference_set()

virtual void flow_insensitive_abstract_domain_baset::get_reference_set ( const namespacet &  , const exprt &  , expr_sett &  expr_set  )

inlinevirtual

Reimplemented in value_set_domain_fit.

Definition at line 67 of file flow_insensitive_analysis.h.

get_return_lhs()

exprt flow_insensitive_abstract_domain_baset::get_return_lhs ( locationt  to ) const

protected

Definition at line 31 of file flow_insensitive_analysis.cpp.

initialize()

virtual void flow_insensitive_abstract_domain_baset::initialize ( const namespacet &  ns )

pure virtual

Implemented in value_set_domain_fit.

output()

virtual void flow_insensitive_abstract_domain_baset::output ( const namespacet &  , std::ostream &    ) const

inlinevirtual

Reimplemented in value_set_domain_fit.

Definition at line 59 of file flow_insensitive_analysis.h.

transform()

virtual bool flow_insensitive_abstract_domain_baset::transform ( const namespacet &  ns, const irep_idt &  function_from, locationt  from, const irep_idt &  function_to, locationt  to  )

pure virtual

Implemented in value_set_domain_fit.

Member Data Documentation

changed

bool flow_insensitive_abstract_domain_baset::changed

protected

Definition at line 79 of file flow_insensitive_analysis.h.

---

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

• /home/runner/work/cbmc/cbmc/src/analyses/flow_insensitive_analysis.h
• /home/runner/work/cbmc/cbmc/src/analyses/flow_insensitive_analysis.cpp