CBMC
Public Member Functions | Public Attributes | List of all members
value_set_domain_fit Class Reference

#include <value_set_domain_fi.h>

+ Inheritance diagram for value_set_domain_fit:
+ Collaboration diagram for value_set_domain_fit:

Public Member Functions

void output (const namespacet &ns, std::ostream &out) const override
 
void initialize (const namespacet &) override
 
bool 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, expr_sett &expr_set) override
 
void clear (void) override
 
- 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_fit 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_hash > expr_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_fi.h.

Member Function Documentation

◆ clear()

void value_set_domain_fit::clear ( void  )
inlineoverridevirtual

Implements flow_insensitive_abstract_domain_baset.

Definition at line 57 of file value_set_domain_fi.h.

◆ get_reference_set()

void value_set_domain_fit::get_reference_set ( const namespacet &  ns,
const exprt &  expr,
expr_sett &  expr_set 
)
inlineoverridevirtual

Reimplemented from flow_insensitive_abstract_domain_baset.

Definition at line 49 of file value_set_domain_fi.h.

◆ initialize()

void value_set_domain_fit::initialize ( const namespacet &  )
inlineoverridevirtual

Implements flow_insensitive_abstract_domain_baset.

Definition at line 37 of file value_set_domain_fi.h.

◆ output()

void value_set_domain_fit::output ( const namespacet &  ns,
std::ostream &  out 
) const
inlineoverridevirtual

Reimplemented from flow_insensitive_abstract_domain_baset.

Definition at line 32 of file value_set_domain_fi.h.

◆ transform()

bool value_set_domain_fit::transform ( const namespacet &  ns,
const irep_idt &  function_from,
locationt  from_l,
const irep_idt &  function_to,
locationt  to_l 
)
overridevirtual

Implements flow_insensitive_abstract_domain_baset.

Definition at line 15 of file value_set_domain_fi.cpp.

Member Data Documentation

◆ value_set

value_set_fit value_set_domain_fit::value_set

Definition at line 23 of file value_set_domain_fi.h.

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