cprover
value_set_domain_fivrnst Class Reference

#include <value_set_domain_fivrns.h>

+ Inheritance diagram for value_set_domain_fivrnst:
+ Collaboration diagram for value_set_domain_fivrnst:

Public Member Functions

virtual void output (const namespacet &ns, std::ostream &out) const
 
virtual void initialize (const namespacet &)
 
virtual bool transform (const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l)
 
virtual void get_reference_set (const namespacet &ns, const exprt &expr, expr_sett &expr_set)
 
virtual void clear (void)
 
- Public Member Functions inherited from flow_insensitive_abstract_domain_baset
 flow_insensitive_abstract_domain_baset ()
 
virtual ~flow_insensitive_abstract_domain_baset ()
 

Public Attributes

value_set_fivrnst value_set
 

Additional Inherited Members

- Public Types inherited from flow_insensitive_abstract_domain_baset
typedef goto_programt::const_targett locationt
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 
- Protected Member Functions inherited from flow_insensitive_abstract_domain_baset
exprt get_guard (locationt from, locationt to) const
 
exprt get_return_lhs (locationt to) const
 
- Protected Attributes inherited from flow_insensitive_abstract_domain_baset
bool changed
 

Detailed Description

Definition at line 20 of file value_set_domain_fivrns.h.

Member Function Documentation

◆ clear()

virtual void value_set_domain_fivrnst::clear ( void  )
inlinevirtual

Implements flow_insensitive_abstract_domain_baset.

Definition at line 56 of file value_set_domain_fivrns.h.

◆ get_reference_set()

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

Reimplemented from flow_insensitive_abstract_domain_baset.

Definition at line 48 of file value_set_domain_fivrns.h.

◆ initialize()

virtual void value_set_domain_fivrnst::initialize ( const namespacet )
inlinevirtual

Implements flow_insensitive_abstract_domain_baset.

Definition at line 35 of file value_set_domain_fivrns.h.

◆ output()

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

Reimplemented from flow_insensitive_abstract_domain_baset.

Definition at line 28 of file value_set_domain_fivrns.h.

◆ transform()

virtual bool value_set_domain_fivrnst::transform ( const namespacet ns,
const irep_idt function_from,
locationt  from_l,
const irep_idt function_to,
locationt  to_l 
)
virtual

Member Data Documentation

◆ value_set

value_set_fivrnst value_set_domain_fivrnst::value_set

Definition at line 24 of file value_set_domain_fivrns.h.


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