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

#include <widened_range.h>

+ Collaboration diagram for widened_ranget:

Public Member Functions

 widened_ranget (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 

Public Attributes

const bool is_lower_widened
 
const bool is_upper_widened
 
const exprt lower_bound
 
const exprt upper_bound
 
const exprt widened_lower_bound
 
const exprt widened_upper_bound
 

Private Member Functions

exprt widen_lower_bound () const
 
exprt widen_upper_bound () const
 

Private Attributes

namespacet ns_
 
exprt range_
 

Detailed Description

Definition at line 17 of file widened_range.h.

Constructor & Destructor Documentation

◆ widened_ranget()

widened_ranget::widened_ranget ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
inline

Definition at line 20 of file widened_range.h.

Member Function Documentation

◆ widen_lower_bound()

exprt widened_ranget::widen_lower_bound ( ) const
private

Definition at line 22 of file widened_range.cpp.

◆ widen_upper_bound()

exprt widened_ranget::widen_upper_bound ( ) const
private

Definition at line 37 of file widened_range.cpp.

Member Data Documentation

◆ is_lower_widened

const bool widened_ranget::is_lower_widened

Definition at line 40 of file widened_range.h.

◆ is_upper_widened

const bool widened_ranget::is_upper_widened

Definition at line 41 of file widened_range.h.

◆ lower_bound

const exprt widened_ranget::lower_bound

Definition at line 42 of file widened_range.h.

◆ ns_

namespacet widened_ranget::ns_
private

Definition at line 46 of file widened_range.h.

◆ range_

exprt widened_ranget::range_
private

Definition at line 47 of file widened_range.h.

◆ upper_bound

const exprt widened_ranget::upper_bound

Definition at line 43 of file widened_range.h.

◆ widened_lower_bound

const exprt widened_ranget::widened_lower_bound

Definition at line 50 of file widened_range.h.

◆ widened_upper_bound

const exprt widened_ranget::widened_upper_bound

Definition at line 51 of file widened_range.h.

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