Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_ARITH_TOOLS_H
11 #define CPROVER_UTIL_ARITH_TOOLS_H
25 DEPRECATED(
"Use the constant_exprt version instead")
38 template <typename Target, typename =
void>
59 typename std::enable_if<std::is_integral<T>::value>::type>
63 template <
typename U = T,
64 typename std::enable_if<std::is_signed<U>::value,
int>::type = 0>
71 template <
typename U = T,
72 typename std::enable_if<!std::is_signed<U>::value,
int>::type = 0>
75 return mpi.to_ulong();
82 #if !defined(_MSC_VER) || _MSC_VER >= 1900
84 std::numeric_limits<T>::max() <=
85 std::numeric_limits<decltype(get_val(mpi))>::max() &&
86 std::numeric_limits<T>::min() >=
87 std::numeric_limits<decltype(get_val(mpi))>::min(),
88 "Numeric cast only works for types smaller than long long");
93 std::numeric_limits<T>::max() <=
94 std::numeric_limits<decltype(get_val(mpi))>::max() &&
95 std::numeric_limits<T>::min() >=
96 std::numeric_limits<decltype(get_val(mpi))>::min());
99 mpi <= std::numeric_limits<T>::max() &&
100 mpi >= std::numeric_limits<T>::min())
102 return static_cast<T>(get_val(mpi));
122 template <
typename Target>
133 template <
typename Target>
137 INVARIANT(maybe,
"mp_integer should be convertible to target integral type");
146 template <
typename Target>
152 "expression should be convertible to target integral type",
171 std::size_t bit_index);
174 make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f);
179 #endif // CPROVER_UTIL_ARITH_TOOLS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
The type of an expression, extends irept.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Numerical cast provides a unified way of converting from one numerical type to another.
Convert expression to mp_integer.
optionalt< T > operator()(const mp_integer &mpi) const
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
optionalt< T > operator()(const exprt &expr) const
const irep_idt & id() const
nonstd::optional< T > optionalt
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
optionalt< mp_integer > operator()(const exprt &expr) const
A constant literal expression.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.