CBMC
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
flow_insensitive_abstract_domain_baset Class Referenceabstract

#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: