CBMC
Public Member Functions | Public Attributes | List of all members
value_set_domain_templatet< VST > Class Template Reference

This is the domain for a value set analysis. More...

#include <value_set_domain.h>

+ Inheritance diagram for value_set_domain_templatet< VST >:
+ Collaboration diagram for value_set_domain_templatet< VST >:

Public Member Functions

bool merge (const value_set_domain_templatet< VST > &other, locationt)
 
void output (const namespacet &, std::ostream &out) const override
 
void initialize (const namespacet &, locationt l) override
 
void transform (const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
 
void get_reference_set (const namespacet &ns, const exprt &expr, value_setst::valuest &dest) override
 
- Public Member Functions inherited from domain_baset
 domain_baset ()
 
virtual ~domain_baset ()
 

Public Attributes

VST value_set
 

Additional Inherited Members

- Public Types inherited from domain_baset
typedef goto_programt::const_targett locationt
 
typedef std::unordered_set< exprt, irep_hash > expr_sett
 
- Protected Attributes inherited from domain_baset
bool seen
 

Detailed Description

template<class VST>
class value_set_domain_templatet< VST >

This is the domain for a value set analysis.

It is intended to be the template parameter for value_set_analysis_templatet, so VST would be value_sett.

Definition at line 24 of file value_set_domain.h.

Member Function Documentation

◆ get_reference_set()

template<class VST >
void value_set_domain_templatet< VST >::get_reference_set ( const namespacet &  ns,
const exprt &  expr,
value_setst::valuest &  dest 
)
inlineoverridevirtual

Reimplemented from domain_baset.

Definition at line 54 of file value_set_domain.h.

◆ initialize()

template<class VST >
void value_set_domain_templatet< VST >::initialize ( const namespacet &  ,
locationt  l 
)
inlineoverridevirtual

Reimplemented from domain_baset.

Definition at line 41 of file value_set_domain.h.

◆ merge()

template<class VST >
bool value_set_domain_templatet< VST >::merge ( const value_set_domain_templatet< VST > &  other,
locationt   
)
inline

Definition at line 31 of file value_set_domain.h.

◆ output()

template<class VST >
void value_set_domain_templatet< VST >::output ( const namespacet &  ,
std::ostream &  out 
) const
inlineoverridevirtual

Reimplemented from domain_baset.

Definition at line 36 of file value_set_domain.h.

◆ transform()

template<class VST >
void value_set_domain_templatet< VST >::transform ( const namespacet &  ns,
const irep_idt &  function_from,
locationt  from_l,
const irep_idt &  function_to,
locationt  to_l 
)
overridevirtual

Implements domain_baset.

Definition at line 66 of file value_set_domain.h.

Member Data Documentation

◆ value_set

template<class VST >
VST value_set_domain_templatet< VST >::value_set

Definition at line 27 of file value_set_domain.h.

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