CBMC
|
#include "arith_tools.h"
#include "c_types.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "invariant.h"
#include "std_expr.h"
#include <algorithm>
Go to the source code of this file.
Functions | |
bool | to_integer (const constant_exprt &expr, mp_integer &int_value) |
Convert a constant expression expr to an arbitrary-precision integer. More... | |
constant_exprt | from_integer (const mp_integer &int_value, const typet &type) |
std::size_t | address_bits (const mp_integer &size) |
ceil(log2(size)) More... | |
mp_integer | power (const mp_integer &base, const mp_integer &exponent) |
A multi-precision implementation of the power operator. More... | |
void | mp_min (mp_integer &a, const mp_integer &b) |
void | mp_max (mp_integer &a, const mp_integer &b) |
bool | get_bvrep_bit (const irep_idt &src, std::size_t width, std::size_t bit_index) |
Get a bit with given index from bit-vector representation. More... | |
static char | nibble2hex (unsigned char nibble) |
turn a value 0...15 into '0'-'9', 'A'-'Z' More... | |
irep_idt | make_bvrep (const std::size_t width, const std::function< bool(std::size_t)> f) |
construct a bit-vector representation from a functor More... | |
irep_idt | bvrep_bitwise_op (const irep_idt &a, const irep_idt &b, const std::size_t width, const std::function< bool(bool, bool)> f) |
perform a binary bit-wise operation, given as a functor, on a bit-vector representation More... | |
irep_idt | bvrep_bitwise_op (const irep_idt &a, const std::size_t width, const std::function< bool(bool)> f) |
perform a unary bit-wise operation, given as a functor, on a bit-vector representation More... | |
irep_idt | integer2bvrep (const mp_integer &src, std::size_t width) |
convert an integer to bit-vector representation with given width This uses two's complement for negative numbers. More... | |
mp_integer | bvrep2integer (const irep_idt &src, std::size_t width, bool is_signed) |
convert a bit-vector representation (possibly signed) to integer More... | |
std::size_t address_bits | ( | const mp_integer & | size | ) |
ceil(log2(size))
Definition at line 177 of file arith_tools.cpp.
mp_integer bvrep2integer | ( | const irep_idt & | src, |
std::size_t | width, | ||
bool | is_signed | ||
) |
convert a bit-vector representation (possibly signed) to integer
Definition at line 402 of file arith_tools.cpp.
irep_idt bvrep_bitwise_op | ( | const irep_idt & | a, |
const irep_idt & | b, | ||
const std::size_t | width, | ||
const std::function< bool(bool, bool)> | f | ||
) |
perform a binary bit-wise operation, given as a functor, on a bit-vector representation
a | the representation of the first bit vector |
b | the representation of the second bit vector |
width | the width of the bit-vector |
f | the functor |
Definition at line 350 of file arith_tools.cpp.
irep_idt bvrep_bitwise_op | ( | const irep_idt & | a, |
const std::size_t | width, | ||
const std::function< bool(bool)> | f | ||
) |
perform a unary bit-wise operation, given as a functor, on a bit-vector representation
a | the bit-vector representation |
width | the width of the bit-vector |
f | the functor |
Definition at line 367 of file arith_tools.cpp.
constant_exprt from_integer | ( | const mp_integer & | int_value, |
const typet & | type | ||
) |
Definition at line 100 of file arith_tools.cpp.
bool get_bvrep_bit | ( | const irep_idt & | src, |
std::size_t | width, | ||
std::size_t | bit_index | ||
) |
Get a bit with given index from bit-vector representation.
src | the bitvector representation |
width | the number of bits in the bitvector |
bit_index | index (0 is the least significant) |
Definition at line 262 of file arith_tools.cpp.
irep_idt integer2bvrep | ( | const mp_integer & | src, |
std::size_t | width | ||
) |
convert an integer to bit-vector representation with given width This uses two's complement for negative numbers.
If the value is out of range, it is 'wrapped around'.
Definition at line 380 of file arith_tools.cpp.
irep_idt make_bvrep | ( | const std::size_t | width, |
const std::function< bool(std::size_t)> | f | ||
) |
construct a bit-vector representation from a functor
width | the width of the bit-vector |
f | the functor – the parameter is the bit index |
Definition at line 306 of file arith_tools.cpp.
void mp_max | ( | mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 252 of file arith_tools.cpp.
void mp_min | ( | mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 246 of file arith_tools.cpp.
|
static |
turn a value 0...15 into '0'-'9', 'A'-'Z'
Definition at line 291 of file arith_tools.cpp.
mp_integer power | ( | const mp_integer & | base, |
const mp_integer & | exponent | ||
) |
A multi-precision implementation of the power operator.
Definition at line 195 of file arith_tools.cpp.
bool to_integer | ( | const constant_exprt & | expr, |
mp_integer & | int_value | ||
) |
Convert a constant expression expr
to an arbitrary-precision integer.
expr | Source expression | |
[out] | int_value | Integer value (only modified if conversion succeeds) |
Definition at line 20 of file arith_tools.cpp.