CBMC
Public Member Functions | Static Private Member Functions | Private Attributes | List of all members
interval_index_ranget Class Reference
+ Inheritance diagram for interval_index_ranget:
+ Collaboration diagram for interval_index_ranget:

Public Member Functions

 interval_index_ranget (const constant_interval_exprt &interval_, const namespacet &n)
 
const exprt & current () const override
 
bool advance_to_next () override
 
index_range_implementation_ptrt reset () const override
 
- Public Member Functions inherited from index_range_implementationt
virtual ~index_range_implementationt ()=default
 

Static Private Member Functions

static exprt next_element (const exprt &cur, const namespacet &ns)
 

Private Attributes

const constant_interval_exprt & interval
 
exprt index
 
exprt next
 
exprt upper
 
const namespacet & ns
 

Detailed Description

Definition at line 27 of file interval_abstract_value.cpp.

Constructor & Destructor Documentation

◆ interval_index_ranget()

interval_index_ranget::interval_index_ranget ( const constant_interval_exprt &  interval_,
const namespacet &  n 
)
inline

Definition at line 30 of file interval_abstract_value.cpp.

Member Function Documentation

◆ advance_to_next()

bool interval_index_ranget::advance_to_next ( )
inlineoverridevirtual

Implements index_range_implementationt.

Definition at line 45 of file interval_abstract_value.cpp.

◆ current()

const exprt& interval_index_ranget::current ( ) const
inlineoverridevirtual

Implements index_range_implementationt.

Definition at line 41 of file interval_abstract_value.cpp.

◆ next_element()

static exprt interval_index_ranget::next_element ( const exprt &  cur,
const namespacet &  ns 
)
inlinestaticprivate

Definition at line 59 of file interval_abstract_value.cpp.

◆ reset()

index_range_implementation_ptrt interval_index_ranget::reset ( ) const
inlineoverridevirtual

Implements index_range_implementationt.

Definition at line 53 of file interval_abstract_value.cpp.

Member Data Documentation

◆ index

exprt interval_index_ranget::index
private

Definition at line 65 of file interval_abstract_value.cpp.

◆ interval

const constant_interval_exprt& interval_index_ranget::interval
private

Definition at line 64 of file interval_abstract_value.cpp.

◆ next

exprt interval_index_ranget::next
private

Definition at line 66 of file interval_abstract_value.cpp.

◆ ns

const namespacet& interval_index_ranget::ns
private

Definition at line 68 of file interval_abstract_value.cpp.

◆ upper

exprt interval_index_ranget::upper
private

Definition at line 67 of file interval_abstract_value.cpp.

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