CBMC
single_value_index_ranget Class Reference

#include <abstract_value_object.h>

+ Inheritance diagram for single_value_index_ranget:
+ Collaboration diagram for single_value_index_ranget:

Public Member Functions

const exprtcurrent () const override
 
bool advance_to_next () override
 
- Public Member Functions inherited from index_range_implementationt
virtual ~index_range_implementationt ()=default
 
virtual index_range_implementation_ptrt reset () const =0
 

Protected Member Functions

 single_value_index_ranget (const exprt &val)
 

Protected Attributes

const exprt value
 

Private Attributes

bool available
 

Detailed Description

Definition at line 109 of file abstract_value_object.h.

Constructor & Destructor Documentation

◆ single_value_index_ranget()

single_value_index_ranget::single_value_index_ranget ( const exprt val)
explicitprotected

Definition at line 59 of file abstract_value_object.cpp.

Member Function Documentation

◆ advance_to_next()

bool single_value_index_ranget::advance_to_next ( )
overridevirtual

Implements index_range_implementationt.

Definition at line 69 of file abstract_value_object.cpp.

◆ current()

const exprt & single_value_index_ranget::current ( ) const
overridevirtual

Implements index_range_implementationt.

Definition at line 64 of file abstract_value_object.cpp.

Member Data Documentation

◆ available

bool single_value_index_ranget::available
private

Definition at line 122 of file abstract_value_object.h.

◆ value

const exprt single_value_index_ranget::value
protected

Definition at line 119 of file abstract_value_object.h.


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