mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

fix a few undefined behaviors exposed by the unit tests

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-05-11 06:30:24 +01:00
parent 091ae37c06
commit 379ce66391
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/bit_util.cpp
View file

@ -351,7 +351,7 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
} }
if (word_sz < sz) { if (word_sz < sz) {
unsigned bit_sz = k % (8 * sizeof(unsigned)); unsigned bit_sz = k % (8 * sizeof(unsigned));
unsigned mask = (1 << bit_sz) - 1; unsigned mask = (1u << bit_sz) - 1;
return (data[word_sz] & mask) != 0; return (data[word_sz] & mask) != 0;
} }
return false; return false;

4
src/util/mpff.cpp
View file

@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) {
} }
else { else {
if (v < 0) { if (v < 0) {
set(n, static_cast<uint64>(-v)); set(n, -static_cast<uint64>(v));
n.m_sign = 1; n.m_sign = 1;
} }
else { else {
@ -680,7 +680,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c
// Make sure that a and b have the same exponent. // Make sure that a and b have the same exponent.
if (exp_a > exp_b) { if (exp_a > exp_b) {
unsigned shift = exp_a - exp_b; unsigned shift = (unsigned)exp_a - (unsigned)exp_b;
n_sig_b = m_buffers[0].c_ptr(); n_sig_b = m_buffers[0].c_ptr();
shr(m_precision, sig_b, shift, m_precision, n_sig_b); shr(m_precision, sig_b, shift, m_precision, n_sig_b);
if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) { if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) {