cprover
flow_insensitive_abstract_domain_baset Class Referenceabstract

#include <flow_insensitive_analysis.h>

Inheritance diagram for flow_insensitive_abstract_domain_baset:
[legend]

Public Types

typedef goto_programt::const_targett locationt
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 

Public Member Functions

 flow_insensitive_abstract_domain_baset ()
 
virtual void initialize (const namespacet &ns)=0
 
virtual bool transform (const namespacet &ns, locationt from, locationt to)=0
 
virtual ~flow_insensitive_abstract_domain_baset ()
 
virtual void output (const namespacet &ns, std::ostream &out) const
 
virtual void get_reference_set (const namespacet &ns, const exprt &expr, 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 25 of file flow_insensitive_analysis.h.

Member Typedef Documentation

§ expr_sett

Definition at line 51 of file flow_insensitive_analysis.h.

§ locationt

Constructor & Destructor Documentation

§ flow_insensitive_abstract_domain_baset()

flow_insensitive_abstract_domain_baset::flow_insensitive_abstract_domain_baset ( )
inline

Definition at line 28 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 41 of file flow_insensitive_analysis.h.

Member Function Documentation

§ clear()

virtual void flow_insensitive_abstract_domain_baset::clear ( void  )
pure virtual

§ get_guard()

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

Definition at line 20 of file flow_insensitive_analysis.cpp.

References exprt::make_not().

§ get_reference_set()

virtual void flow_insensitive_abstract_domain_baset::get_reference_set ( const namespacet ns,
const exprt expr,
expr_sett expr_set 
)
inlinevirtual

§ get_return_lhs()

exprt flow_insensitive_abstract_domain_baset::get_return_lhs ( locationt  to) const
protected

§ initialize()

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

§ output()

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

§ transform()

virtual bool flow_insensitive_abstract_domain_baset::transform ( const namespacet ns,
locationt  from,
locationt  to 
)
pure virtual

Member Data Documentation

§ changed

bool flow_insensitive_abstract_domain_baset::changed
protected

Definition at line 65 of file flow_insensitive_analysis.h.

Referenced by flow_insensitive_analysis_baset::visit().


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