cprover
value_set_domain_templatet< VST > Class Template Reference

#include <value_set_domain.h>

Inheritance diagram for value_set_domain_templatet< VST >:
[legend]
Collaboration diagram for value_set_domain_templatet< VST >:
[legend]

Public Member Functions

bool merge (const value_set_domain_templatet< VST > &other, locationt to)
 
virtual void output (const namespacet &ns, std::ostream &out) const
 
virtual void initialize (const namespacet &ns, locationt l)
 
virtual void transform (const namespacet &ns, locationt from_l, locationt to_l)
 
virtual void get_reference_set (const namespacet &ns, const exprt &expr, value_setst::valuest &dest)
 
- 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_hashexpr_sett
 
- Protected Attributes inherited from domain_baset
bool seen
 

Detailed Description

template<class VST>
class value_set_domain_templatet< VST >

Definition at line 21 of file value_set_domain.h.

Member Function Documentation

◆ get_reference_set()

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

Reimplemented from domain_baset.

Definition at line 53 of file value_set_domain.h.

References value_set_domain_templatet< VST >::value_set.

◆ initialize()

template<class VST>
virtual void value_set_domain_templatet< VST >::initialize ( const namespacet ns,
locationt  l 
)
inlinevirtual

Reimplemented from domain_baset.

Definition at line 40 of file value_set_domain.h.

References value_set_domain_templatet< VST >::value_set.

◆ merge()

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

Definition at line 28 of file value_set_domain.h.

References value_set_domain_templatet< VST >::value_set.

◆ output()

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

Reimplemented from domain_baset.

Definition at line 33 of file value_set_domain.h.

References value_set_domain_templatet< VST >::value_set.

◆ transform()

template<class VST>
virtual void value_set_domain_templatet< VST >::transform ( const namespacet ns,
locationt  from_l,
locationt  to_l 
)
virtual

Implements domain_baset.

Member Data Documentation

◆ value_set


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