cprover
mp_arith.cpp File Reference
#include "mp_arith.h"
#include <cassert>
#include <cctype>
#include <cstdlib>
#include <limits>
#include <ostream>
#include <sstream>
#include <vector>
#include "arith_tools.h"
#include "invariant.h"
Include dependency graph for mp_arith.cpp:

Go to the source code of this file.

Typedefs

typedef BigInt::ullong_t ullong_t
 
typedef BigInt::llong_t llong_t
 

Functions

mp_integer operator>> (const mp_integer &a, const mp_integer &b)
 
mp_integer operator<< (const mp_integer &a, const mp_integer &b)
 
std::ostream & operator<< (std::ostream &out, const mp_integer &n)
 
const mp_integer string2integer (const std::string &n, unsigned base)
 
const std::string integer2binary (const mp_integer &n, std::size_t width)
 
const std::string integer2string (const mp_integer &n, unsigned base)
 
const mp_integer binary2integer (const std::string &n, bool is_signed)
 convert binary string representation to mp_integer More...
 
mp_integer::ullong_t integer2ulong (const mp_integer &n)
 
std::size_t integer2size_t (const mp_integer &n)
 
unsigned integer2unsigned (const mp_integer &n)
 
mp_integer bitwise_or (const mp_integer &a, const mp_integer &b)
 bitwise or bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer bitwise_and (const mp_integer &a, const mp_integer &b)
 bitwise and bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer bitwise_xor (const mp_integer &a, const mp_integer &b)
 bitwise xor bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer bitwise_neg (const mp_integer &a)
 bitwise negation bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer arith_left_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 arithmetic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer arith_right_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer logic_left_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 logic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer logic_right_shift (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer rotate_right (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 
mp_integer rotate_left (const mp_integer &a, const mp_integer &b, std::size_t true_size)
 rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long) More...
 

Typedef Documentation

◆ llong_t

typedef BigInt::llong_t llong_t

Definition at line 23 of file mp_arith.cpp.

◆ ullong_t

typedef BigInt::ullong_t ullong_t

Definition at line 22 of file mp_arith.cpp.

Function Documentation

◆ arith_left_shift()

mp_integer arith_left_shift ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

arithmetic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 254 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ arith_right_shift()

mp_integer arith_right_shift ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 275 of file mp_arith.cpp.

References pad(), PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ binary2integer()

◆ bitwise_and()

mp_integer bitwise_and ( const mp_integer a,
const mp_integer b 
)

bitwise and bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 224 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ bitwise_neg()

mp_integer bitwise_neg ( const mp_integer a)

bitwise negation bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 244 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ bitwise_or()

mp_integer bitwise_or ( const mp_integer a,
const mp_integer b 
)

bitwise or bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 214 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ bitwise_xor()

mp_integer bitwise_xor ( const mp_integer a,
const mp_integer b 
)

bitwise xor bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 234 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ integer2binary()

◆ integer2size_t()

std::size_t integer2size_t ( const mp_integer )
Deprecated:
use numeric_cast_v<std::size_t> instead

Definition at line 195 of file mp_arith.cpp.

References PRECONDITION.

Referenced by add_padding(), add_padding_gcc(), add_padding_msvc(), as_vcd_binary(), interpretert::assign(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), endianness_mapt::build_little_endian(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_unbounded_array(), boolbvt::convert_byte_update(), boolbvt::convert_extractbit(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), boolbvt::convert_shift(), boolbvt::convert_update_rec(), boolbvt::convert_with_bv(), c_typecheck_baset::designator_enter(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_rec(), interpretert::evaluate(), interpretert::execute_assign(), expr_initializert< nondet >::expr_initializer_rec(), flatten_byte_update(), rw_range_sett::get_objects_byte_extract(), interpretert::get_value(), lower_popcount(), c_typecheck_baset::make_designator(), smt2_convt::parse_rec(), interpretert::read_unbounded(), remove_vector(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), ieee_floatt::to_string_decimal(), remove_const_function_pointerst::try_resolve_index_of(), c_typecheck_baset::typecheck_c_bit_field_type(), and java_bytecode_convert_methodt::variable().

◆ integer2string()

◆ integer2ulong()

◆ integer2unsigned()

◆ logic_left_shift()

mp_integer logic_left_shift ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

logic left shift bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 295 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

◆ logic_right_shift()

mp_integer logic_right_shift ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 321 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ operator<<() [1/2]

mp_integer operator<< ( const mp_integer a,
const mp_integer b 
)

Definition at line 43 of file mp_arith.cpp.

References power().

◆ operator<<() [2/2]

std::ostream& operator<< ( std::ostream &  out,
const mp_integer n 
)

Definition at line 48 of file mp_arith.cpp.

References integer2string().

◆ operator>>()

mp_integer operator>> ( const mp_integer a,
const mp_integer b 
)

Definition at line 25 of file mp_arith.cpp.

References power().

◆ rotate_left()

mp_integer rotate_left ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 358 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ rotate_right()

mp_integer rotate_right ( const mp_integer a,
const mp_integer b,
std::size_t  true_size 
)

rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest object size should be the largest available c++ integer size (currently long long)

Definition at line 338 of file mp_arith.cpp.

References PRECONDITION, and messaget::result().

Referenced by interpretert::evaluate().

◆ string2integer()