CBMC: abstract_object_sett Class Reference

CBMC

Loading...

Searching...

No Matches

Public Types | Public Member Functions | Private Attributes | List of all members

abstract_object_sett Class Reference

#include <abstract_object_set.h>

+ Collaboration diagram for abstract_object_sett:

Public Types

using value_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, abstract_equalert >

using const_iterator = value_sett::const_iterator

using value_type = value_sett::value_type

using size_type = value_sett::size_type

Public Member Functions

void insert (const abstract_object_pointert &o)

void insert (abstract_object_pointert &&o)

void insert (const abstract_object_sett &rhs)

void insert (const value_ranget &rhs)

void push_back (const abstract_object_pointert &v)

abstract_object_pointert first () const

const_iterator begin () const

const_iterator end () const

value_sett::size_type size () const

bool empty () const

bool operator== (const abstract_object_sett &rhs) const

void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const

constant_interval_exprt to_interval () const

Calculate the set of values as an interval.

Private Attributes

value_sett values

Detailed Description

Definition at line 18 of file abstract_object_set.h.

Member Typedef Documentation

◆ const_iterator

using abstract_object_sett::const_iterator = value_sett::const_iterator

Definition at line 25 of file abstract_object_set.h.

◆ size_type

using abstract_object_sett::size_type = value_sett::size_type

Definition at line 27 of file abstract_object_set.h.

◆ value_sett

using abstract_object_sett::value_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, abstract_equalert>

Definition at line 21 of file abstract_object_set.h.

◆ value_type

using abstract_object_sett::value_type = value_sett::value_type

Definition at line 26 of file abstract_object_set.h.

Member Function Documentation

◆ begin()

const_iterator abstract_object_sett::begin ( ) const

inline

Definition at line 58 of file abstract_object_set.h.

◆ clear()

void abstract_object_sett::clear ( )

inline

Definition at line 81 of file abstract_object_set.h.

◆ empty()

bool abstract_object_sett::empty ( ) const

inline

Definition at line 71 of file abstract_object_set.h.

◆ end()

const_iterator abstract_object_sett::end ( ) const

inline

Definition at line 62 of file abstract_object_set.h.

◆ first()

abstract_object_pointert abstract_object_sett::first ( ) const

inline

Definition at line 53 of file abstract_object_set.h.

◆ insert() [1/4]

void abstract_object_sett::insert ( abstract_object_pointert && o )

inline

Definition at line 33 of file abstract_object_set.h.

◆ insert() [2/4]

void abstract_object_sett::insert ( const abstract_object_pointert & o )

inline

Definition at line 29 of file abstract_object_set.h.

◆ insert() [3/4]

void abstract_object_sett::insert ( const abstract_object_sett & rhs )

inline

Definition at line 37 of file abstract_object_set.h.

◆ insert() [4/4]

void abstract_object_sett::insert ( const value_ranget & rhs )

inline

Definition at line 41 of file abstract_object_set.h.

◆ operator==()

bool abstract_object_sett::operator== ( const abstract_object_sett & rhs ) const

inline

Definition at line 76 of file abstract_object_set.h.

◆ output()

void abstract_object_sett::output ( std::ostream & out,

const ai_baset & ai,

const namespacet & ns

) const

Definition at line 25 of file abstract_object_set.cpp.

◆ push_back()

void abstract_object_sett::push_back ( const abstract_object_pointert & v )

inline

Definition at line 47 of file abstract_object_set.h.

◆ size()

value_sett::size_type abstract_object_sett::size ( ) const

inline

Definition at line 67 of file abstract_object_set.h.

◆ to_interval()

constant_interval_exprt abstract_object_sett::to_interval ( ) const

Calculate the set of values as an interval.

Returns: the constant_interval_exprt bounding the values

Definition at line 42 of file abstract_object_set.cpp.

Member Data Documentation

◆ values

value_sett abstract_object_sett::values

private

Definition at line 94 of file abstract_object_set.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_object_set.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_object_set.cpp

abstract_object_sett
Generated by doxygen 1.9.8