|
CBMC
|
#include "invariant.h"#include "mp_arith.h"#include "optional.h"#include "std_expr.h"#include <limits>
Include dependency graph for arith_tools.h:Go to the source code of this file.
Classes | |
| struct | numeric_castt< Target, typename > |
| Numerical cast provides a unified way of converting from one numerical type to another. More... | |
| struct | numeric_castt< mp_integer > |
| Convert expression to mp_integer. More... | |
| struct | numeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type > |
| Convert mp_integer or expr to any integral type. More... | |
Functions | |
| bool | to_integer (const constant_exprt &expr, mp_integer &int_value) |
Convert a constant expression expr to an arbitrary-precision integer. More... | |
| template<typename Target > | |
| optionalt< Target > | numeric_cast (const exprt &arg) |
| Converts an expression to any integral type. More... | |
| template<typename Target > | |
| Target | numeric_cast_v (const mp_integer &arg) |
| Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possible. More... | |
| template<typename Target > | |
| Target | numeric_cast_v (const constant_exprt &arg) |
| Convert an expression to integral type Target An invariant will fail if the conversion is not possible. 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... | |
| 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 | integer2bvrep (const mp_integer &, 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 &, 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 & | , |
| 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.
| 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.
Converts an expression to any integral type.
| Target | type to convert to |
| arg | expression to convert |
Definition at line 125 of file arith_tools.h.
| Target numeric_cast_v | ( | const constant_exprt & | arg | ) |
Convert an expression to integral type Target An invariant will fail if the conversion is not possible.
| Target | type to convert to |
| arg | constant expression |
Definition at line 149 of file arith_tools.h.
| Target numeric_cast_v | ( | const mp_integer & | arg | ) |
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possible.
| Target | type to convert to |
| arg | mp_integer |
Definition at line 136 of file arith_tools.h.
| 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.