Static Value-Flow Analysis
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Friends | List of all members
SVF::BoundedInt Class Reference

A class representing a bounded 64-bit integer. More...

#include <NumericValue.h>

Public Member Functions

 BoundedInt (s64_t fVal)
 
 BoundedInt (s64_t fVal, bool isInf)
 
 BoundedInt (const BoundedInt &rhs)
 
BoundedIntoperator= (const BoundedInt &rhs)
 
 BoundedInt (BoundedInt &&rhs)
 
BoundedIntoperator= (BoundedInt &&rhs)
 
virtual ~BoundedInt ()
 
bool is_plus_infinity () const
 
bool is_minus_infinity () const
 
bool is_infinity () const
 
void set_plus_infinity ()
 
void set_minus_infinity ()
 
bool is_zero () const
 
bool equal (const BoundedInt &rhs) const
 
bool leq (const BoundedInt &rhs) const
 
bool geq (const BoundedInt &rhs) const
 
bool is_true () const
 
s64_t getNumeral () const
 Retrieves the numeral value of the BoundedInt object. More...
 
virtual const std::string to_string () const
 
bool is_real () const
 
s64_t getIntNumeral () const
 
double getRealNumeral () const
 
const double getFVal () const
 

Static Public Member Functions

static BoundedInt plus_infinity ()
 
static BoundedInt minus_infinity ()
 
static bool isZero (const BoundedInt &expr)
 
static BoundedInt safeAdd (const BoundedInt &lhs, const BoundedInt &rhs)
 
static BoundedInt safeMul (const BoundedInt &lhs, const BoundedInt &rhs)
 Performs safe multiplication of two BoundedInt objects. More...
 
static BoundedInt min (std::vector< BoundedInt > &_l)
 
static BoundedInt max (std::vector< BoundedInt > &_l)
 

Protected Member Functions

 BoundedInt ()=default
 

Protected Attributes

s64_t _iVal
 
bool _isInf
 

Friends

BoundedInt operator== (const BoundedInt &lhs, const BoundedInt &rhs)
 Reload operator. More...
 
BoundedInt operator!= (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator> (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator< (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator<= (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator>= (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator+ (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator- (const BoundedInt &lhs)
 
BoundedInt operator- (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator% (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator* (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator/ (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator^ (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator& (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator| (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator&& (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator|| (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator! (const BoundedInt &lhs)
 
BoundedInt operator>> (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt operator<< (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt ite (const BoundedInt &cond, const BoundedInt &lhs, const BoundedInt &rhs)
 
std::ostream & operator<< (std::ostream &out, const BoundedInt &expr)
 
bool eq (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt min (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt max (const BoundedInt &lhs, const BoundedInt &rhs)
 
BoundedInt abs (const BoundedInt &lhs)
 

Detailed Description

A class representing a bounded 64-bit integer.

BoundedInt is a class that represents a 64-bit integer that can also represent positive and negative infinity. It includes a 64-bit integer value and a boolean flag indicating whether the value is infinite. If the value is infinite, the integer value is used to represent the sign of infinity (1 for positive infinity and 0 for negative infinity).

Definition at line 54 of file NumericValue.h.

Constructor & Destructor Documentation

◆ BoundedInt() [1/5]

SVF::BoundedInt::BoundedInt ( )
protecteddefault

◆ BoundedInt() [2/5]

SVF::BoundedInt::BoundedInt ( s64_t  fVal)
inline

Definition at line 69 of file NumericValue.h.

69 : _iVal(fVal), _isInf(false) {}

◆ BoundedInt() [3/5]

SVF::BoundedInt::BoundedInt ( s64_t  fVal,
bool  isInf 
)
inline

Definition at line 73 of file NumericValue.h.

73 : _iVal(fVal), _isInf(isInf) {}

◆ BoundedInt() [4/5]

SVF::BoundedInt::BoundedInt ( const BoundedInt rhs)
inline

Definition at line 76 of file NumericValue.h.

76 : _iVal(rhs._iVal), _isInf(rhs._isInf) {}

◆ BoundedInt() [5/5]

SVF::BoundedInt::BoundedInt ( BoundedInt &&  rhs)
inline

Definition at line 87 of file NumericValue.h.

87 : _iVal(rhs._iVal), _isInf(rhs._isInf) {}

◆ ~BoundedInt()

virtual SVF::BoundedInt::~BoundedInt ( )
inlinevirtual

Definition at line 98 of file NumericValue.h.

98 {}

Member Function Documentation

◆ equal()

bool SVF::BoundedInt::equal ( const BoundedInt rhs) const
inline

Definition at line 155 of file NumericValue.h.

156  {
157  return _iVal == rhs._iVal && _isInf == rhs._isInf;
158  }

◆ geq()

bool SVF::BoundedInt::geq ( const BoundedInt rhs) const
inline

Definition at line 189 of file NumericValue.h.

190  {
191  // If only one of the two BoundedInts is infinite.
192  if (is_infinity() ^ rhs.is_infinity())
193  {
194  if (is_infinity())
195  {
196  return is_plus_infinity();
197  }
198  else
199  {
200  return rhs.is_minus_infinity();
201  }
202  }
203  // If both BoundedInts are infinite.
204  if (is_infinity() && rhs.is_infinity())
205  {
206  if (is_plus_infinity())
207  return true;
208  else
209  return rhs.is_minus_infinity();
210  }
211  // If neither BoundedInt is infinite.
212  else
213  return _iVal >= rhs._iVal;
214  }
bool is_plus_infinity() const
Definition: NumericValue.h:101
bool is_infinity() const
Definition: NumericValue.h:113

◆ getFVal()

const double SVF::BoundedInt::getFVal ( ) const
inline

Definition at line 714 of file NumericValue.h.

715  {
716  assert(false && "cannot get real number for integer!");
717  abort();
718  }

◆ getIntNumeral()

s64_t SVF::BoundedInt::getIntNumeral ( ) const
inline

Definition at line 703 of file NumericValue.h.

704  {
705  return getNumeral();
706  }
s64_t getNumeral() const
Retrieves the numeral value of the BoundedInt object.
Definition: NumericValue.h:661

◆ getNumeral()

s64_t SVF::BoundedInt::getNumeral ( ) const
inline

Retrieves the numeral value of the BoundedInt object.

This method returns the numeral representation of the BoundedInt object. If the object represents negative infinity, it returns the minimum representable 64-bit integer. If the object represents positive infinity, it returns the maximum representable 64-bit integer. Otherwise, it returns the actual 64-bit integer value of the object.

Returns
The numeral value of the BoundedInt object.

Definition at line 661 of file NumericValue.h.

662  {
663  // If the object represents negative infinity, return the minimum
664  // representable 64-bit integer.
665  if (is_minus_infinity())
666  {
667  return std::numeric_limits<s64_t>::min();
668  }
669  // If the object represents positive infinity, return the maximum
670  // representable 64-bit integer.
671  else if (is_plus_infinity())
672  {
673  return std::numeric_limits<s64_t>::max();
674  }
675  // Otherwise, return the actual 64-bit integer value of the object.
676  else
677  {
678  return _iVal;
679  }
680  }
bool is_minus_infinity() const
Definition: NumericValue.h:107

◆ getRealNumeral()

double SVF::BoundedInt::getRealNumeral ( ) const
inline

Definition at line 708 of file NumericValue.h.

709  {
710  assert(false && "cannot get real number for integer!");
711  abort();
712  }

◆ is_infinity()

bool SVF::BoundedInt::is_infinity ( ) const
inline

Definition at line 113 of file NumericValue.h.

114  {
115  return is_plus_infinity() || is_minus_infinity();
116  }

◆ is_minus_infinity()

bool SVF::BoundedInt::is_minus_infinity ( ) const
inline

Definition at line 107 of file NumericValue.h.

108  {
109  return _isInf && _iVal == -1;
110  }

◆ is_plus_infinity()

bool SVF::BoundedInt::is_plus_infinity ( ) const
inline

Definition at line 101 of file NumericValue.h.

102  {
103  return _isInf && _iVal == 1;
104  }

◆ is_real()

bool SVF::BoundedInt::is_real ( ) const
inline

Definition at line 698 of file NumericValue.h.

699  {
700  return false;
701  }

◆ is_true()

bool SVF::BoundedInt::is_true ( ) const
inline

Definition at line 645 of file NumericValue.h.

646  {
647  return _iVal != 0;
648  }

◆ is_zero()

bool SVF::BoundedInt::is_zero ( ) const
inline

Definition at line 143 of file NumericValue.h.

144  {
145  return _iVal == 0;
146  }

◆ isZero()

static bool SVF::BoundedInt::isZero ( const BoundedInt expr)
inlinestatic

Definition at line 149 of file NumericValue.h.

150  {
151  return expr._iVal == 0;
152  }

◆ leq()

bool SVF::BoundedInt::leq ( const BoundedInt rhs) const
inline

Definition at line 161 of file NumericValue.h.

162  {
163  // If only one of the two BoundedInts is infinite.
164  if (is_infinity() ^ rhs.is_infinity())
165  {
166  if (is_infinity())
167  {
168  return is_minus_infinity();
169  }
170  else
171  {
172  return rhs.is_plus_infinity();
173  }
174  }
175  // If both BoundedInts are infinite.
176  if (is_infinity() && rhs.is_infinity())
177  {
178  if (is_minus_infinity())
179  return true;
180  else
181  return rhs.is_plus_infinity();
182  }
183  // If neither BoundedInt is infinite.
184  else
185  return _iVal <= rhs._iVal;
186  }

◆ max()

static BoundedInt SVF::BoundedInt::max ( std::vector< BoundedInt > &  _l)
inlinestatic

Definition at line 619 of file NumericValue.h.

620  {
621  BoundedInt ret(minus_infinity());
622  for (const auto& it : _l)
623  {
624  if (it.is_plus_infinity())
625  return plus_infinity();
626  else if (!it.leq(ret))
627  {
628  ret = it;
629  }
630  }
631  return ret;
632  }
BoundedInt()=default
static BoundedInt plus_infinity()
Definition: NumericValue.h:131
static BoundedInt minus_infinity()
Definition: NumericValue.h:137

◆ min()

static BoundedInt SVF::BoundedInt::min ( std::vector< BoundedInt > &  _l)
inlinestatic

Definition at line 601 of file NumericValue.h.

602  {
603  BoundedInt ret(plus_infinity());
604  for (const auto& it : _l)
605  {
606  if (it.is_minus_infinity())
607  return minus_infinity();
608  else if (!it.geq(ret))
609  {
610  ret = it;
611  }
612  }
613  return ret;
614  }

◆ minus_infinity()

static BoundedInt SVF::BoundedInt::minus_infinity ( )
inlinestatic

Definition at line 137 of file NumericValue.h.

138  {
139  return {-1, true};
140  }

◆ operator=() [1/2]

BoundedInt& SVF::BoundedInt::operator= ( BoundedInt &&  rhs)
inline

Definition at line 90 of file NumericValue.h.

91  {
92  _iVal = rhs._iVal;
93  _isInf = rhs._isInf;
94  return *this;
95  }

◆ operator=() [2/2]

BoundedInt& SVF::BoundedInt::operator= ( const BoundedInt rhs)
inline

Definition at line 79 of file NumericValue.h.

80  {
81  _iVal = rhs._iVal;
82  _isInf = rhs._isInf;
83  return *this;
84  }

◆ plus_infinity()

static BoundedInt SVF::BoundedInt::plus_infinity ( )
inlinestatic

Definition at line 131 of file NumericValue.h.

132  {
133  return {1, true};
134  }

◆ safeAdd()

static BoundedInt SVF::BoundedInt::safeAdd ( const BoundedInt lhs,
const BoundedInt rhs 
)
inlinestatic

Safely adds two BoundedInt objects.

This function adds two BoundedInt objects in a way that respects the bounds of the underlying s64_t type. It checks for conditions that would result in overflow or underflow and returns a representation of positive or negative infinity in those cases. If addition of the two numbers would result in a value that is within the representable range of s64_t, it performs the addition and returns the result. If the addition is not defined (e.g., positive infinity plus negative infinity), it asserts false to indicate an error.

Parameters
lhsThe first BoundedInt to add. This can be any valid BoundedInt, including positive and negative infinity.
rhsThe second BoundedInt to add. This can be any valid BoundedInt, including positive and negative infinity.
Returns
A BoundedInt that represents the result of the addition. If the addition would result in overflow, the function returns a BoundedInt representing positive infinity. If the addition would result in underflow, the function returns a BoundedInt representing negative infinity. If the addition is not defined (e.g., positive infinity plus negative infinity), the function asserts false and does not return a value.

Definition at line 280 of file NumericValue.h.

281  {
282  // If one number is positive infinity and the other is negative
283  // infinity, this is an invalid operation, so we assert false.
284  if ((lhs.is_plus_infinity() && rhs.is_minus_infinity()) ||
285  (lhs.is_minus_infinity() && rhs.is_plus_infinity()))
286  {
287  assert(false && "invalid add");
288  }
289 
290  // If either number is positive infinity, the result is positive
291  // infinity.
292  if (lhs.is_plus_infinity() || rhs.is_plus_infinity())
293  {
294  return plus_infinity();
295  }
296 
297  // If either number is negative infinity, the result is negative
298  // infinity.
299  if (lhs.is_minus_infinity() || rhs.is_minus_infinity())
300  {
301  return minus_infinity();
302  }
303 
304  // If both numbers are positive and their sum would exceed the maximum
305  // representable number, the result is positive infinity.
306  if (lhs._iVal > 0 && rhs._iVal > 0 &&
307  (std::numeric_limits<s64_t>::max() - lhs._iVal) < rhs._iVal)
308  {
309  return plus_infinity();
310  }
311 
312  // If both numbers are negative and their sum would be less than the
313  // most negative representable number, the result is negative infinity.
314  if (lhs._iVal < 0 && rhs._iVal < 0 &&
315  (-std::numeric_limits<s64_t>::max() - lhs._iVal) > rhs._iVal)
316  {
317  return minus_infinity();
318  }
319 
320  // If none of the above conditions are met, the numbers can be safely
321  // added.
322  return lhs._iVal + rhs._iVal;
323  }

◆ safeMul()

static BoundedInt SVF::BoundedInt::safeMul ( const BoundedInt lhs,
const BoundedInt rhs 
)
inlinestatic

Performs safe multiplication of two BoundedInt objects.

This function ensures that the multiplication of two BoundedInt objects doesn't result in overflow or underflow. It returns the multiplication result if it can be represented within the range of a 64-bit integer. If the result would be larger than the maximum representable positive number, it returns positive infinity. If the result would be less than the minimum representable negative number, it returns negative infinity. If either of the inputs is zero, the result is zero. If either of the inputs is infinity, the result is determined by the signs of the inputs.

Parameters
lhsThe first BoundedInt to multiply.
rhsThe second BoundedInt to multiply.
Returns
The result of the multiplication, or positive/negative infinity if the result would be outside the range of a 64-bit integer.

Definition at line 364 of file NumericValue.h.

365  {
366  // If either number is zero, the result is zero.
367  if (lhs._iVal == 0 || rhs._iVal == 0)
368  return 0;
369 
370  // If either number is infinity, the result depends on the signs of the
371  // numbers.
372  if (lhs.is_infinity() || rhs.is_infinity())
373  {
374  // If the signs of the numbers are the same, the result is positive
375  // infinity. If the signs of the numbers are different, the result
376  // is negative infinity.
377  if (lhs._iVal * rhs._iVal > 0)
378  {
379  return plus_infinity();
380  }
381  else
382  {
383  return minus_infinity();
384  }
385  }
386 
387  // If both numbers are positive and their product would exceed the
388  // maximum representable number, the result is positive infinity.
389  if (lhs._iVal > 0 && rhs._iVal > 0 &&
390  (std::numeric_limits<s64_t>::max() / lhs._iVal) < rhs._iVal)
391  {
392  return plus_infinity();
393  }
394 
395  // If both numbers are negative and their product would exceed the
396  // maximum representable number, the result is positive infinity.
397  if (lhs._iVal < 0 && rhs._iVal < 0 &&
398  (std::numeric_limits<s64_t>::max() / lhs._iVal) > rhs._iVal)
399  {
400  return plus_infinity();
401  }
402 
403  // If one number is positive and the other is negative and their product
404  // would be less than the most negative representable number, the result
405  // is negative infinity.
406  if ((lhs._iVal > 0 && rhs._iVal < 0 &&
407  (-std::numeric_limits<s64_t>::max() / lhs._iVal) > rhs._iVal) ||
408  (lhs._iVal < 0 && rhs._iVal > 0 &&
409  (-std::numeric_limits<s64_t>::max() / rhs._iVal) > lhs._iVal))
410  {
411  return minus_infinity();
412  }
413 
414  // If none of the above conditions are met, the numbers can be safely
415  // multiplied.
416  return lhs._iVal * rhs._iVal;
417  }

◆ set_minus_infinity()

void SVF::BoundedInt::set_minus_infinity ( )
inline

Definition at line 125 of file NumericValue.h.

126  {
127  *this = minus_infinity();
128  }

◆ set_plus_infinity()

void SVF::BoundedInt::set_plus_infinity ( )
inline

Definition at line 119 of file NumericValue.h.

120  {
121  *this = plus_infinity();
122  }

◆ to_string()

virtual const std::string SVF::BoundedInt::to_string ( ) const
inlinevirtual

Definition at line 682 of file NumericValue.h.

683  {
684  if (is_minus_infinity())
685  {
686  return "-oo";
687  }
688  if (is_plus_infinity())
689  {
690  return "+oo";
691  }
692  else
693  return std::to_string(_iVal);
694  }

Friends And Related Function Documentation

◆ abs

BoundedInt abs ( const BoundedInt lhs)
friend

Definition at line 637 of file NumericValue.h.

638  {
639  return lhs.leq(0) ? -lhs : lhs;
640  }

◆ eq

bool eq ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 561 of file NumericValue.h.

562  {
563  return lhs._iVal == rhs._iVal && lhs._isInf == rhs._isInf;
564  }

◆ ite

BoundedInt ite ( const BoundedInt cond,
const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 543 of file NumericValue.h.

545  {
546  return cond._iVal != 0 ? lhs : rhs;
547  }

◆ max

BoundedInt max ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 585 of file NumericValue.h.

586  {
587  if (lhs.is_plus_infinity() || rhs.is_plus_infinity())
588  return plus_infinity();
589  else if(lhs.is_minus_infinity())
590  return rhs;
591  else if(rhs.is_minus_infinity())
592  return lhs;
593  else
594  return BoundedInt(std::max(lhs._iVal, rhs._iVal));
595  }

◆ min

BoundedInt min ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 569 of file NumericValue.h.

570  {
571  if (lhs.is_minus_infinity() || rhs.is_minus_infinity())
572  return minus_infinity();
573  else if(lhs.is_plus_infinity())
574  return rhs;
575  else if(rhs.is_plus_infinity())
576  return lhs;
577  else
578  return BoundedInt(std::min(lhs._iVal, rhs._iVal));
579  }

◆ operator!

BoundedInt operator! ( const BoundedInt lhs)
friend

Definition at line 499 of file NumericValue.h.

500  {
501  return !lhs._iVal;
502  }

◆ operator!=

BoundedInt operator!= ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 225 of file NumericValue.h.

226  {
227  return !lhs.equal(rhs);
228  }

◆ operator%

BoundedInt operator% ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 420 of file NumericValue.h.

421  {
422  if (rhs.is_zero())
423  assert(false && "divide by zero");
424  else if (!lhs.is_infinity() && !rhs.is_infinity())
425  return lhs._iVal % rhs._iVal;
426  else if (!lhs.is_infinity() && rhs.is_infinity())
427  return 0;
428  // TODO: not sure
429  else if (lhs.is_infinity() && !rhs.is_infinity())
430  return ite(rhs._iVal > 0, lhs, -lhs);
431  else
432  // TODO: +oo/-oo L'Hôpital's rule?
433  return eq(lhs, rhs) ? plus_infinity() : minus_infinity();
434  abort();
435  }
friend BoundedInt ite(const BoundedInt &cond, const BoundedInt &lhs, const BoundedInt &rhs)
Definition: NumericValue.h:543
friend bool eq(const BoundedInt &lhs, const BoundedInt &rhs)
Definition: NumericValue.h:561

◆ operator&

BoundedInt operator& ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 471 of file NumericValue.h.

472  {
473  return lhs._iVal & rhs._iVal;
474  }

◆ operator&&

BoundedInt operator&& ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 487 of file NumericValue.h.

488  {
489  return lhs._iVal && rhs._iVal;
490  }

◆ operator*

BoundedInt operator* ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 438 of file NumericValue.h.

439  {
440  return safeMul(lhs, rhs);
441  }
static BoundedInt safeMul(const BoundedInt &lhs, const BoundedInt &rhs)
Performs safe multiplication of two BoundedInt objects.
Definition: NumericValue.h:364

◆ operator+

BoundedInt operator+ ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 327 of file NumericValue.h.

328  {
329  return safeAdd(lhs, rhs);
330  }
static BoundedInt safeAdd(const BoundedInt &lhs, const BoundedInt &rhs)
Definition: NumericValue.h:280

◆ operator- [1/2]

BoundedInt operator- ( const BoundedInt lhs)
friend

Definition at line 334 of file NumericValue.h.

335  {
336  return {-lhs._iVal, lhs._isInf};
337  }

◆ operator- [2/2]

BoundedInt operator- ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 342 of file NumericValue.h.

343  {
344  return safeAdd(lhs, -rhs);
345  }

◆ operator/

BoundedInt operator/ ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 446 of file NumericValue.h.

447  {
448  if (rhs.is_zero())
449  assert(false && "divide by zero");
450  else if (!lhs.is_infinity() && !rhs.is_infinity())
451  return lhs._iVal / rhs._iVal;
452  else if (!lhs.is_infinity() && rhs.is_infinity())
453  return 0;
454  else if (lhs.is_infinity() && !rhs.is_infinity())
455  return ite(rhs._iVal >= 0, lhs, -lhs);
456  else
457  return eq(lhs, rhs) ? plus_infinity() : minus_infinity();
458  }

◆ operator<

BoundedInt operator< ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 237 of file NumericValue.h.

238  {
239  return !lhs.geq(rhs);
240  }

◆ operator<< [1/2]

BoundedInt operator<< ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 527 of file NumericValue.h.

528  {
529  assert(rhs.geq(0) && "rhs should be greater or equal than 0");
530  if (lhs.is_zero())
531  return lhs;
532  else if (lhs.is_infinity())
533  return lhs;
534  else if (rhs.is_infinity())
535  return lhs.geq(0) ? plus_infinity() : minus_infinity();
536  else
537  return lhs._iVal << rhs._iVal;
538  }

◆ operator<< [2/2]

std::ostream& operator<< ( std::ostream &  out,
const BoundedInt expr 
)
friend

Definition at line 552 of file NumericValue.h.

553  {
554  out << expr._iVal;
555  return out;
556  }

◆ operator<=

BoundedInt operator<= ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 244 of file NumericValue.h.

245  {
246  return lhs.leq(rhs);
247  }

◆ operator==

BoundedInt operator== ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Reload operator.

Definition at line 219 of file NumericValue.h.

220  {
221  return lhs.equal(rhs);
222  }

◆ operator>

BoundedInt operator> ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 231 of file NumericValue.h.

232  {
233  return !lhs.leq(rhs);
234  }

◆ operator>=

BoundedInt operator>= ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 251 of file NumericValue.h.

252  {
253  return lhs.geq(rhs);
254  }

◆ operator>>

BoundedInt operator>> ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 509 of file NumericValue.h.

510  {
511  assert(rhs.geq(0) && "rhs should be greater or equal than 0");
512  if (lhs.is_zero())
513  return lhs;
514  else if (lhs.is_infinity())
515  return lhs;
516  else if (rhs.is_infinity())
517  return lhs.geq(0) ? 0 : -1;
518  else
519  return lhs._iVal >> rhs._iVal;
520  }

◆ operator^

BoundedInt operator^ ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 465 of file NumericValue.h.

466  {
467  return lhs._iVal ^ rhs._iVal;
468  }

◆ operator|

BoundedInt operator| ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 477 of file NumericValue.h.

478  {
479  return lhs._iVal | rhs._iVal;
480  }

◆ operator||

BoundedInt operator|| ( const BoundedInt lhs,
const BoundedInt rhs 
)
friend

Definition at line 493 of file NumericValue.h.

494  {
495  return lhs._iVal || rhs._iVal;
496  }

Member Data Documentation

◆ _isInf

bool SVF::BoundedInt::_isInf
protected

Definition at line 58 of file NumericValue.h.

◆ _iVal

s64_t SVF::BoundedInt::_iVal
protected

Definition at line 57 of file NumericValue.h.


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