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

#include <static_analysis.h>

+ Inheritance diagram for domain_baset:

Public Types

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

Public Member Functions

 domain_baset ()
 
virtual ~domain_baset ()
 
virtual void initialize (const namespacet &, locationt)
 
virtual void transform (const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
 
virtual void output (const namespacet &, std::ostream &) const
 
virtual void get_reference_set (const namespacet &, const exprt &, std::list< exprt > &dest)
 

Protected Attributes

bool seen
 

Friends

class static_analysis_baset
 

Detailed Description

Definition at line 30 of file static_analysis.h.

Member Typedef Documentation

◆ expr_sett

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

Definition at line 72 of file static_analysis.h.

◆ locationt

typedef goto_programt::const_targett domain_baset::locationt

Definition at line 41 of file static_analysis.h.

Constructor & Destructor Documentation

◆ domain_baset()

domain_baset::domain_baset ( )
inline

Definition at line 33 of file static_analysis.h.

◆ ~domain_baset()

virtual domain_baset::~domain_baset ( )
inlinevirtual

Definition at line 37 of file static_analysis.h.

Member Function Documentation

◆ get_reference_set()

virtual void domain_baset::get_reference_set ( const namespacet &  ,
const exprt &  ,
std::list< exprt > &  dest 
)
inlinevirtual

Reimplemented in value_set_domain_templatet< VST >.

Definition at line 75 of file static_analysis.h.

◆ initialize()

virtual void domain_baset::initialize ( const namespacet &  ,
locationt   
)
inlinevirtual

Reimplemented in value_set_domain_templatet< VST >.

Definition at line 45 of file static_analysis.h.

◆ output()

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

Reimplemented in value_set_domain_templatet< VST >.

Definition at line 66 of file static_analysis.h.

◆ transform()

virtual void 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_templatet< VST >.

Friends And Related Function Documentation

◆ static_analysis_baset

friend class static_analysis_baset
friend

Definition at line 94 of file static_analysis.h.

Member Data Documentation

◆ seen

bool domain_baset::seen
protected

Definition at line 92 of file static_analysis.h.

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