From 0e1bdf5a09dd363f1bcff32a43906f65ef4da066 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Feb 2025 12:37:36 +0000 Subject: [PATCH 01/18] Remove unused {c,java}_qualifierst::count These are never used (and their implementation was awkwardly summing up Booleans, yielding conversion warnings). --- jbmc/src/java_bytecode/java_qualifiers.cpp | 5 ----- jbmc/src/java_bytecode/java_qualifiers.h | 1 - src/ansi-c/c_qualifiers.h | 6 ------ 3 files changed, 12 deletions(-) diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/jbmc/src/java_bytecode/java_qualifiers.cpp index d146580cc91..38a4acb77d1 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.cpp +++ b/jbmc/src/java_bytecode/java_qualifiers.cpp @@ -27,11 +27,6 @@ std::unique_ptr java_qualifierst::clone() const return std::move(other); } -std::size_t java_qualifierst::count() const -{ - return c_qualifierst::count() + annotations.size(); -} - void java_qualifierst::clear() { c_qualifierst::clear(); diff --git a/jbmc/src/java_bytecode/java_qualifiers.h b/jbmc/src/java_bytecode/java_qualifiers.h index 8e61ad187e6..da58c7e5959 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.h +++ b/jbmc/src/java_bytecode/java_qualifiers.h @@ -31,7 +31,6 @@ class java_qualifierst : public c_qualifierst { return annotations; } - std::size_t count() const override; void clear() override; diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h index 3c403dcadb3..2cf17bb2161 100644 --- a/src/ansi-c/c_qualifiers.h +++ b/src/ansi-c/c_qualifiers.h @@ -109,12 +109,6 @@ class c_qualifierst is_noreturn |= other.is_noreturn; return *this; } - - virtual std::size_t count() const - { - return is_constant + is_volatile + is_restricted + is_atomic + is_ptr32 + - is_ptr64 + is_nodiscard + is_noreturn; - } }; #endif // CPROVER_ANSI_C_C_QUALIFIERS_H From f569d0070d4044cd7f760cab9f420b719525142e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Feb 2025 13:00:56 +0000 Subject: [PATCH 02/18] Cleanup type conversions in java_bytecode_parsert::read We can safely read signed values and don't need to defer the type conversion to the call site. --- .../java_bytecode/java_bytecode_parser.cpp | 44 ++++++++++++------- 1 file changed, 27 insertions(+), 17 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index e036b06bdc4..c1f5a383aac 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -132,9 +132,19 @@ class java_bytecode_parsert final : public parsert T read() { static_assert( - std::is_unsigned::value, "T should be an unsigned integer"); + std::is_unsigned::value || std::is_signed::value, + "T should be a signed or unsigned integer"); const constexpr size_t bytes = sizeof(T); - u8 result = 0; + if(bytes == 1) + { + if(!*in) + { + log.error() << "unexpected end of bytecode file" << messaget::eom; + throw 0; + } + return static_cast(in->get()); + } + T result = 0; for(size_t i = 0; i < bytes; i++) { if(!*in) @@ -145,7 +155,7 @@ class java_bytecode_parsert final : public parsert result <<= 8u; result |= static_cast(in->get()); } - return narrow_cast(result); + return result; } void store_unknown_method_handle(size_t bootstrap_method_index); @@ -700,7 +710,7 @@ void java_bytecode_parsert::rconstant_pool() std::string s; s.resize(bytes); for(auto &ch : s) - ch = read(); + ch = read(); it->s = s; // Add to string table } break; @@ -942,7 +952,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) case 'b': // a signed byte { - const s1 c = read(); + const s1 c = read(); instruction.args.push_back(from_integer(c, signedbv_typet(8))); } address+=1; @@ -950,7 +960,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) case 'o': // two byte branch offset, signed { - const s2 offset = read(); + const s2 offset = read(); // By converting the signed offset into an absolute address (by adding // the current address) the number represented becomes unsigned. instruction.args.push_back( @@ -961,7 +971,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) case 'O': // four byte branch offset, signed { - const s4 offset = read(); + const s4 offset = read(); // By converting the signed offset into an absolute address (by adding // the current address) the number represented becomes unsigned. instruction.args.push_back( @@ -994,7 +1004,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) { const u2 v = read(); instruction.args.push_back(from_integer(v, unsignedbv_typet(16))); - const s2 c = read(); + const s2 c = read(); instruction.args.push_back(from_integer(c, signedbv_typet(16))); address+=4; } @@ -1002,7 +1012,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) { const u1 v = read(); instruction.args.push_back(from_integer(v, unsignedbv_typet(8))); - const s1 c = read(); + const s1 c = read(); instruction.args.push_back(from_integer(c, signedbv_typet(8))); address+=2; } @@ -1032,7 +1042,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) } // now default value - const s4 default_value = read(); + const s4 default_value = read(); // By converting the signed offset into an absolute address (by adding // the current address) the number represented becomes unsigned. instruction.args.push_back( @@ -1045,8 +1055,8 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) for(std::size_t i=0; i(); - const s4 offset = read(); + const s4 match = read(); + const s4 offset = read(); instruction.args.push_back( from_integer(match, signedbv_typet(32))); // By converting the signed offset into an absolute address (by adding @@ -1070,23 +1080,23 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) } // now default value - const s4 default_value = read(); + const s4 default_value = read(); instruction.args.push_back( from_integer(base_offset+default_value, signedbv_typet(32))); address+=4; // now low value - const s4 low_value = read(); + const s4 low_value = read(); address+=4; // now high value - const s4 high_value = read(); + const s4 high_value = read(); address+=4; // there are high-low+1 offsets, and they are signed for(s4 i=low_value; i<=high_value; i++) { - s4 offset = read(); + s4 offset = read(); instruction.args.push_back(from_integer(i, signedbv_typet(32))); // By converting the signed offset into an absolute address (by adding // the current address) the number represented becomes unsigned. @@ -1130,7 +1140,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) case 's': // a signed short { - const s2 s = read(); + const s2 s = read(); instruction.args.push_back(from_integer(s, signedbv_typet(16))); } address+=2; From e0e192c0fc64aa4c931b056c6de1f856c0e1e44f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Jun 2018 19:38:05 +0100 Subject: [PATCH 03/18] Consistently use unsigned in big-int --- src/big-int/bigint.cc | 116 ++++++++++++++++++++------------------- unit/big-int/big-int.cpp | 6 +- 2 files changed, 63 insertions(+), 59 deletions(-) diff --git a/src/big-int/bigint.cc b/src/big-int/bigint.cc index 978c63e2ad0..33e555bf2d1 100644 --- a/src/big-int/bigint.cc +++ b/src/big-int/bigint.cc @@ -58,13 +58,13 @@ adjust_size (unsigned size) inline int digit_cmp (onedig_t const *a, onedig_t const *b, unsigned n) { - for (int i = n; --i >= 0; ) - { - if (a[i] < b[i]) - return -1; - else if (a[i] > b[i]) - return 1; - } + for(unsigned i = n; i > 0; --i) + { + if(a[i - 1] < b[i - 1]) + return -1; + else if(a[i - 1] > b[i - 1]) + return 1; + } return 0; } @@ -136,12 +136,12 @@ static _fast onedig_t digit_mul (onedig_t *b, unsigned l, onedig_t d) { twodig_t p = 0; - for (int i = l; --i >= 0; ) - { - p += twodig_t (d) * twodig_t (*b); - *b++ = onedig_t (p); - p >>= single_bits; - } + for(unsigned i = l; i > 0; --i) + { + p += twodig_t(d) * twodig_t(*b); + *b++ = onedig_t(p); + p >>= single_bits; + } return onedig_t (p); } @@ -177,13 +177,13 @@ static _fast onedig_t digit_div (onedig_t *b, unsigned l, onedig_t d) { twodig_t r = 0; - for (int i = l; --i >= 0; ) - { - r <<= single_bits; - r |= b[i]; - b[i] = onedig_t (r / d); - r %= d; - } + for(unsigned i = l; i > 0; --i) + { + r <<= single_bits; + r |= b[i - 1]; + b[i - 1] = onedig_t(r / d); + r %= d; + } return onedig_t (r); } @@ -259,17 +259,18 @@ static _fast void digit_div (onedig_t *r, const onedig_t *y, unsigned yl, onedig_t *q, unsigned ql) { r += ql; - for (int i = ql; --r, --i >= 0; ) + --r; + for(unsigned i = ql; i > 0; --r, --i) + { + onedig_t qh = guess_q(r + yl, y + yl - 1); + if(multiply_and_subtract(r, y, yl, qh) == 0) { - onedig_t qh = guess_q (r + yl, y + yl - 1); - if (multiply_and_subtract (r, y, yl, qh) == 0) - { - --qh; - add_back (r, y, yl); - } - if (q != 0) - q[i] = qh; + --qh; + add_back(r, y, yl); } + if(q != 0) + q[i - 1] = qh; + } } @@ -502,16 +503,16 @@ BigInt::scan_on (char const *s, onedig_t b) for (char c = *s; c; c = *++s) { // Convert digit. Use 0..9A..Z for singles up to 36. Ignoring case. - c = toupper (c); + c = (char)toupper(c); onedig_t dig; if (c < '0') return s; else if (c <= '9') - dig = c - '0'; + dig = (onedig_t)(c - '0'); else if (c < 'A') return s; else if (c <= 'Z') - dig = c - 'A' + 10; + dig = (onedig_t)(c - 'A' + 10); else return s; if (dig >= b) @@ -585,7 +586,7 @@ BigInt::as_string (char *p, unsigned l, onedig_t b) const if (l == 0) return 0; onedig_t r = digit_div (dig, len, b); - p[--l] = r < 10 ? r + '0' : 'A' + r - 10; + p[--l] = (char)(r < 10 ? r + '0' : 'A' + r - 10); if (dig[len-1] == 0) --len; } @@ -632,7 +633,7 @@ BigInt::dump (unsigned char *p, unsigned n) for (;;) { while (i--) - *p++ = d >> i * CHAR_BIT; + *p++ = (unsigned char)(d >> i * CHAR_BIT); if (t <= digit) break; d = *--t; @@ -683,8 +684,8 @@ BigInt::is_long() const return false; // There is exactly one good signed number n with abs (n) having the // topmost bit set: The most negative number. - for (int l = length - 1; --l >= 0; ) - if (digit[l] != 0) + for(unsigned l = length - 1; l > 0; --l) + if(digit[l - 1] != 0) return false; return true; } @@ -692,18 +693,18 @@ BigInt::is_long() const ullong_t BigInt::to_ulong() const { ullong_t ul = 0; - for (int i = length; --i >= 0; ) - { - ul <<= single_bits; - ul |= digit[i]; - } + for(unsigned i = length; i > 0; --i) + { + ul <<= single_bits; + ul |= digit[i - 1]; + } return ul; } llong_t BigInt::to_long() const { - ullong_t ul = to_ulong(); - return positive ? ul : -llong_t (ul); + llong_t l = llong_t(to_ulong()); + return positive ? l : -l; } @@ -753,7 +754,7 @@ BigInt::compare (llong_t b) const onedig_t dig[small]; unsigned len; - digit_set (-b, dig, len); + digit_set(ullong_t(-b), dig, len); if (length < len) return 1; if (length > len) @@ -905,7 +906,7 @@ BigInt & BigInt::operator+= (llong_t y) { bool pos = y > 0; - ullong_t uy = pos ? y : -y; + ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; unsigned yl; digit_set (uy, yb, yl); @@ -917,7 +918,7 @@ BigInt & BigInt::operator-= (llong_t y) { bool pos = y > 0; - ullong_t uy = pos ? y : -y; + ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; unsigned yl; digit_set (uy, yb, yl); @@ -929,7 +930,7 @@ BigInt & BigInt::operator*= (llong_t y) { bool pos = y > 0; - ullong_t uy = pos ? y : -y; + ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; unsigned yl; digit_set (uy, yb, yl); @@ -941,7 +942,7 @@ BigInt & BigInt::operator/= (llong_t y) { bool pos = y > 0; - ullong_t uy = pos ? y : -y; + ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; unsigned yl; digit_set (uy, yb, yl); @@ -952,7 +953,7 @@ BigInt & BigInt::operator%= (llong_t y) { bool pos = y > 0; - ullong_t uy = pos ? y : -y; + ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; unsigned yl; digit_set (uy, yb, yl); @@ -1078,7 +1079,7 @@ BigInt::div (BigInt const &x, BigInt const &y, BigInt &q, BigInt &r) // This digit_div() transforms the dividend into the quotient. q = y; r.digit[0] = digit_div (q.digit, q.length, y.digit[0]); - r.length = r.digit[0] ? 1 : 0; + r.length = r.digit[0] ? 1u : 0u; } else { @@ -1269,22 +1270,25 @@ BigInt::operator%= (BigInt const &y) unsigned BigInt::floorPow2 () const { - int i = length - 1; // Start on the last value - while (i >= 0 && digit[i] == 0) { + unsigned i = length; // Start on the last value + while(i > 0 && digit[i - 1] == 0) + { --i; // Skip zeros } - if (i < 0) { + if(i == 0) + { return 0; // Special case } twodig_t power = 1; - int count = 0; + unsigned count = 0; - while ((power << 1) <= (twodig_t)digit[i]) { + while((power << 1) <= (twodig_t)digit[i - 1]) + { ++count, power <<= 1; } - return (single_bits * i) + count; + return (single_bits * (i - 1)) + count; } // Not part of original BigInt. diff --git a/unit/big-int/big-int.cpp b/unit/big-int/big-int.cpp index 678318bf238..ab678018a71 100644 --- a/unit/big-int/big-int.cpp +++ b/unit/big-int/big-int.cpp @@ -245,12 +245,12 @@ TEST_CASE("arbitrary precision integers", "[core][big-int][bigint]") REQUIRE(N == M); - REQUIRE(N.floorPow2() == 0); + REQUIRE(N.floorPow2() == 0U); N -= 1; // 0 - REQUIRE(N.floorPow2() == 0); + REQUIRE(N.floorPow2() == 0U); N += 2; // 2 - REQUIRE(N.floorPow2() == 1); + REQUIRE(N.floorPow2() == 1U); } } From db6d5e5b91271f919fc5829d79520e0590ba25c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Feb 2025 13:34:39 +0000 Subject: [PATCH 04/18] Use std::size_t for all size-typed operations in big-int --- src/big-int/bigint-func.cc | 4 +- src/big-int/bigint.cc | 242 ++++++++++++++++++------------------- src/big-int/bigint.hh | 30 ++--- src/util/mp_arith.cpp | 2 +- 4 files changed, 132 insertions(+), 146 deletions(-) diff --git a/src/big-int/bigint-func.cc b/src/big-int/bigint-func.cc index 6ee5210a5c6..8eb293960fc 100644 --- a/src/big-int/bigint-func.cc +++ b/src/big-int/bigint-func.cc @@ -7,9 +7,7 @@ #include "bigint.hh" - -BigInt -pow (BigInt const &x, unsigned y) +BigInt pow(BigInt const &x, std::size_t y) { BigInt a = x; BigInt r = 1; diff --git a/src/big-int/bigint.cc b/src/big-int/bigint.cc index 33e555bf2d1..158e51a540c 100644 --- a/src/big-int/bigint.cc +++ b/src/big-int/bigint.cc @@ -25,13 +25,11 @@ typedef BigInt::onedig_t onedig_t; typedef BigInt::twodig_t twodig_t; static const unsigned small = BigInt::small; -static const int single_bits = sizeof (onedig_t) * CHAR_BIT; +static const std::size_t single_bits = sizeof(onedig_t) * CHAR_BIT; static const twodig_t base = twodig_t (1) << single_bits; static const twodig_t single_max = base - 1; - -inline unsigned -adjust_size (unsigned size) +inline std::size_t adjust_size(std::size_t size) { // Always allocate at least something greater than an ullong_t. if (size <= small) @@ -40,8 +38,8 @@ adjust_size (unsigned size) // Assuming the heap works with a specific granularity G and needs // space B for a few bookkeeping pointers: Prefer allocation sizes // of N * G - B. (Just guesses. May tune that later.) - const unsigned G = 32; - const unsigned B = 8; + const std::size_t G = 32; + const std::size_t B = 8; size *= sizeof (onedig_t); size += B; size += G - 1; @@ -55,10 +53,9 @@ adjust_size (unsigned size) // Compare unsigned digit strings, returns -1/0/+1. -inline int -digit_cmp (onedig_t const *a, onedig_t const *b, unsigned n) +inline int digit_cmp(onedig_t const *a, onedig_t const *b, std::size_t n) { - for(unsigned i = n; i > 0; --i) + for(std::size_t i = n; i > 0; --i) { if(a[i - 1] < b[i - 1]) return -1; @@ -70,13 +67,15 @@ digit_cmp (onedig_t const *a, onedig_t const *b, unsigned n) // Add unsigned digit strings, return carry. Assumes l1 >= l2! -static _fast onedig_t -digit_add (onedig_t const *d1, unsigned l1, - onedig_t const *d2, unsigned l2, - onedig_t *r) // May be same as d1 or d2. +static _fast onedig_t digit_add( + onedig_t const *d1, + std::size_t l1, + onedig_t const *d2, + std::size_t l2, + onedig_t *r) // May be same as d1 or d2. { twodig_t c = 0; - unsigned i = 0; + std::size_t i = 0; while (i < l2) { c += twodig_t (d1[i]) + twodig_t (d2[i]); @@ -101,13 +100,15 @@ digit_add (onedig_t const *d1, unsigned l1, // Subtract unsigned digit strings, return carry. Assumes l1 >= l2! -static _fast void -digit_sub (onedig_t const *d1, unsigned l1, - onedig_t const *d2, unsigned l2, - onedig_t *r) // May be same as d1 or d2. +static _fast void digit_sub( + onedig_t const *d1, + std::size_t l1, + onedig_t const *d2, + std::size_t l2, + onedig_t *r) // May be same as d1 or d2. { twodig_t c = 1; - unsigned i = 0; + std::size_t i = 0; while (i < l2) { c += twodig_t (d1[i]) + single_max - twodig_t (d2[i]); @@ -132,11 +133,10 @@ digit_sub (onedig_t const *d1, unsigned l1, // Multiply unsigned digit string by single digit, replaces argument // with product and returns overflowing digit. -static _fast onedig_t -digit_mul (onedig_t *b, unsigned l, onedig_t d) +static _fast onedig_t digit_mul(onedig_t *b, std::size_t l, onedig_t d) { twodig_t p = 0; - for(unsigned i = l; i > 0; --i) + for(std::size_t i = l; i > 0; --i) { p += twodig_t(d) * twodig_t(*b); *b++ = onedig_t(p); @@ -149,35 +149,36 @@ digit_mul (onedig_t *b, unsigned l, onedig_t d) // Multiply two digit strings. Writes result into a third digit string // which must have the appropriate size and must not be same as one of // the arguments. -static _fast void -digit_mul (onedig_t const *a, unsigned la, - onedig_t const *b, unsigned lb, - onedig_t *r) // Must not be same as a or b. +static _fast void digit_mul( + onedig_t const *a, + std::size_t la, + onedig_t const *b, + std::size_t lb, + onedig_t *r) // Must not be same as a or b. { memset (r, 0, (la + lb) * sizeof (onedig_t)); - for (unsigned i = 0; i < la; i++) + for(std::size_t i = 0; i < la; i++) + { + onedig_t d = a[i]; + twodig_t p = 0; + for(std::size_t j = 0; j < lb; j++) { - onedig_t d = a[i]; - twodig_t p = 0; - for (unsigned j = 0; j < lb; j++) - { - p += r[j] + twodig_t (d) * b[j]; - r[j] = onedig_t (p); - p >>= single_bits; - } - r[lb] = onedig_t (p); - ++r; + p += r[j] + twodig_t(d) * b[j]; + r[j] = onedig_t(p); + p >>= single_bits; } + r[lb] = onedig_t(p); + ++r; + } } // Divide unsigned digit string by single digit, replaces argument // with quotient and returns remainder. -static _fast onedig_t -digit_div (onedig_t *b, unsigned l, onedig_t d) +static _fast onedig_t digit_div(onedig_t *b, std::size_t l, onedig_t d) { twodig_t r = 0; - for(unsigned i = l; i > 0; --i) + for(std::size_t i = l; i > 0; --i) { r <<= single_bits; r |= b[i - 1]; @@ -216,20 +217,20 @@ guess_q (onedig_t const *r, onedig_t const *y) // Multiply divisor with quotient digit and subtract from dividend. // Returns overflow. static _fast onedig_t -multiply_and_subtract (onedig_t *r, onedig_t const *y, unsigned l, onedig_t q) +multiply_and_subtract(onedig_t *r, onedig_t const *y, std::size_t l, onedig_t q) { twodig_t p = 0; twodig_t h = 1; - for (unsigned i = 0; i < l; i++) - { - p += twodig_t (q) * y[i]; - h += r[i]; - h += single_max; - h -= onedig_t (p); - r[i] = onedig_t (h); - p >>= single_bits; - h >>= single_bits; - } + for(std::size_t i = 0; i < l; i++) + { + p += twodig_t(q) * y[i]; + h += r[i]; + h += single_max; + h -= onedig_t(p); + r[i] = onedig_t(h); + p >>= single_bits; + h >>= single_bits; + } h += r[l]; h += single_max; h -= p; @@ -239,28 +240,31 @@ multiply_and_subtract (onedig_t *r, onedig_t const *y, unsigned l, onedig_t q) // Add back divisor digits to dividend, corresponds to a correction of // the guessed quotient digit by -1. -static _fast void -add_back (onedig_t *r, onedig_t const *y, unsigned l) +static _fast void add_back(onedig_t *r, onedig_t const *y, std::size_t l) { twodig_t h = 0; - for (unsigned i = 0; i < l; i++) - { - h += r[i]; - h += y[i]; - r[i] = onedig_t (h); - h >>= single_bits; - } + for(std::size_t i = 0; i < l; i++) + { + h += r[i]; + h += y[i]; + r[i] = onedig_t(h); + h >>= single_bits; + } r[l] = 0; } // Divide two digit strings. Divides r by y/yl. Stores quotient in // q/ql and leaves the remainder in r. Size of r is yl+ql. -static _fast void -digit_div (onedig_t *r, const onedig_t *y, unsigned yl, onedig_t *q, unsigned ql) +static _fast void digit_div( + onedig_t *r, + const onedig_t *y, + std::size_t yl, + onedig_t *q, + std::size_t ql) { r += ql; --r; - for(unsigned i = ql; i > 0; --r, --i) + for(std::size_t i = ql; i > 0; --r, --i) { onedig_t qh = guess_q(r + yl, y + yl - 1); if(multiply_and_subtract(r, y, yl, qh) == 0) @@ -276,8 +280,7 @@ digit_div (onedig_t *r, const onedig_t *y, unsigned yl, onedig_t *q, unsigned ql // Newly allocate uninitialized space for specified number of digits. -inline void -BigInt::allocate (unsigned digits) +inline void BigInt::allocate(std::size_t digits) { size = adjust_size (digits); length = 0; @@ -288,8 +291,7 @@ BigInt::allocate (unsigned digits) // Used in assignment: When smaller than specified digits, allocate // anew. Don`t bother to keep the contents. -inline void -BigInt::reallocate (unsigned digits) +inline void BigInt::reallocate(std::size_t digits) { if (digits > size) { @@ -303,13 +305,12 @@ BigInt::reallocate (unsigned digits) // Increase size keeping the contents. -inline void -BigInt::resize (unsigned digits) +inline void BigInt::resize(std::size_t digits) { if (digits > size) { onedig_t *old_digit = digit; - unsigned old_size = size; + std::size_t old_size = size; size = adjust_size (digits); digit = new onedig_t[size]; if (old_digit) @@ -342,8 +343,7 @@ BigInt::adjust() // Store unsigned elementary integer type into string of onedig_t. -inline void -digit_set (ullong_t ul, onedig_t d[small], unsigned &l) +inline void digit_set(ullong_t ul, onedig_t d[small], std::size_t &l) { l = 0; if (ul) @@ -395,11 +395,8 @@ BigInt::~BigInt() } } -BigInt::BigInt (onedig_t *dig, unsigned len, bool pos) - : size (0), - length (len), - digit (dig), - positive (pos) +BigInt::BigInt(onedig_t *dig, std::size_t len, bool pos) + : size(0), length(len), digit(dig), positive(pos) {} BigInt::BigInt() @@ -551,9 +548,7 @@ BigInt::scan (char const *s, onedig_t b) return scan_on (s, b); } - -unsigned -BigInt::digits (onedig_t b) const +std::size_t BigInt::digits(onedig_t b) const { int bits = -1; while (b) @@ -561,15 +556,13 @@ BigInt::digits (onedig_t b) const return (single_bits * length + bits - 1) / bits; } - -char * -BigInt::as_string (char *p, unsigned l, onedig_t b) const +char *BigInt::as_string(char *p, std::size_t l, onedig_t b) const { if (l < 2) return 0; // Not enough room for number. p[--l] = '\0'; // Check for zero. Would otherwise print as empty string. - unsigned len = length; + std::size_t len = length; while (len && digit[len-1] == 0) --len; if (len == 0) @@ -602,8 +595,7 @@ BigInt::as_string (char *p, unsigned l, onedig_t b) const return p + l; } -bool -BigInt::dump (unsigned char *p, unsigned n) +bool BigInt::dump(unsigned char *p, std::size_t n) { // Access most significant digit. onedig_t *t = digit + length; @@ -617,9 +609,9 @@ BigInt::dump (unsigned char *p, unsigned n) } // Determine number m of characters needed. onedig_t d = *--t; - unsigned i = sizeof (onedig_t); + std::size_t i = sizeof(onedig_t); while (--i && (d >> i * CHAR_BIT) == 0); - unsigned m = ++i + (t - digit) * sizeof (onedig_t); + const std::size_t m = ++i + (t - digit) * sizeof(onedig_t); // Fill in leading zeroes. if (m > n) { @@ -642,8 +634,7 @@ BigInt::dump (unsigned char *p, unsigned n) return true; } -void -BigInt::load (unsigned char const *p, unsigned n) +void BigInt::load(unsigned char const *p, std::size_t n) { // Skip leading zeroes. while (n > 0 && *p == 0) @@ -654,7 +645,7 @@ BigInt::load (unsigned char const *p, unsigned n) length = 0; unsigned char const *q = p + n; onedig_t d = 0; - unsigned i = 0; + std::size_t i = 0; for (;;) { if (q <= p) @@ -684,7 +675,7 @@ BigInt::is_long() const return false; // There is exactly one good signed number n with abs (n) having the // topmost bit set: The most negative number. - for(unsigned l = length - 1; l > 0; --l) + for(std::size_t l = length - 1; l > 0; --l) if(digit[l - 1] != 0) return false; return true; @@ -693,7 +684,7 @@ BigInt::is_long() const ullong_t BigInt::to_ulong() const { ullong_t ul = 0; - for(unsigned i = length; i > 0; --i) + for(std::size_t i = length; i > 0; --i) { ul <<= single_bits; ul |= digit[i - 1]; @@ -729,7 +720,7 @@ BigInt::compare (ullong_t b) const if (!positive) return -1; onedig_t dig[small]; - unsigned len; + std::size_t len; digit_set (b, dig, len); if (length < len) return -1; @@ -753,7 +744,7 @@ BigInt::compare (llong_t b) const return 1; onedig_t dig[small]; - unsigned len; + std::size_t len; digit_set(ullong_t(-b), dig, len); if (length < len) return 1; @@ -777,8 +768,7 @@ BigInt::compare (BigInt const &b) const // Auxiliary method for all adding and subtracting. -void -BigInt::add (onedig_t const *dig, unsigned len, bool pos) +void BigInt::add(onedig_t const *dig, std::size_t len, bool pos) { // Make sure the result fits into this, even with carry. resize ((length > len ? length : len) + 1); @@ -787,7 +777,7 @@ BigInt::add (onedig_t const *dig, unsigned len, bool pos) // expect the greater operand first. onedig_t const *d1; onedig_t const *d2; - unsigned l1, l2; + std::size_t l1, l2; bool gt = (length > len || (length == len && digit_cmp (digit, dig, len) >= 0)); if (gt) @@ -830,8 +820,7 @@ BigInt::add (onedig_t const *dig, unsigned len, bool pos) // Auxiliary method for multiplication. -void -BigInt::mul (onedig_t const *dig, unsigned len, bool pos) +void BigInt::mul(onedig_t const *dig, std::size_t len, bool pos) { if (len < 2) { @@ -875,7 +864,7 @@ BigInt::mul (onedig_t const *dig, unsigned len, bool pos) else { // Get a new string of digits for the result. - unsigned old_size = size; + std::size_t old_size = size; size = adjust_size (length + len); onedig_t *r = new onedig_t[size]; @@ -908,7 +897,7 @@ BigInt::operator+= (llong_t y) bool pos = y > 0; ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); add (yb, yl, pos); return *this; @@ -920,7 +909,7 @@ BigInt::operator-= (llong_t y) bool pos = y > 0; ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); add (yb, yl, !pos); return *this; @@ -932,7 +921,7 @@ BigInt::operator*= (llong_t y) bool pos = y > 0; ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); mul (yb, yl, pos); return *this; @@ -944,7 +933,7 @@ BigInt::operator/= (llong_t y) bool pos = y > 0; ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); return *this /= BigInt (yb, yl, pos); } @@ -955,7 +944,7 @@ BigInt::operator%= (llong_t y) bool pos = y > 0; ullong_t uy = pos ? ullong_t(y) : ullong_t(-y); onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); return *this %= BigInt (yb, yl, pos); } @@ -965,7 +954,7 @@ BigInt & BigInt::operator+= (ullong_t uy) { onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); add (yb, yl, true); return *this; @@ -975,7 +964,7 @@ BigInt & BigInt::operator-= (ullong_t uy) { onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); add (yb, yl, false); return *this; @@ -985,7 +974,7 @@ BigInt & BigInt::operator*= (ullong_t uy) { onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); mul (yb, yl, true); return *this; @@ -995,7 +984,7 @@ BigInt & BigInt::operator/= (ullong_t uy) { onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); return *this /= BigInt (yb, yl, true); } @@ -1004,7 +993,7 @@ BigInt & BigInt::operator%= (ullong_t uy) { onedig_t yb[small]; - unsigned yl; + std::size_t yl; digit_set (uy, yb, yl); return *this %= BigInt (yb, yl, true); } @@ -1086,11 +1075,11 @@ BigInt::div (BigInt const &x, BigInt const &y, BigInt &q, BigInt &r) // Copy operands and scale them such that the first divisor // digit is initially no less than half base. This is essential // for guess_q() to work. - unsigned al = x.length; + std::size_t al = x.length; onedig_t *a = (onedig_t *)alloca ((al + 2) * sizeof (onedig_t)); memcpy (a, x.digit, al * sizeof (onedig_t)); - unsigned bl = y.length; + std::size_t bl = y.length; onedig_t *b = (onedig_t *)alloca (bl * sizeof (onedig_t)); memcpy (b, y.digit, bl * sizeof (onedig_t)); @@ -1169,11 +1158,11 @@ BigInt::operator/= (BigInt const &y) else { // Copy and scale as above in div(). - unsigned al = length; + std::size_t al = length; onedig_t *a = (onedig_t *)alloca ((al + 2) * sizeof (onedig_t)); memcpy (a, digit, al * sizeof (onedig_t)); - unsigned bl = y.length; + std::size_t bl = y.length; onedig_t *b = (onedig_t *)alloca (bl * sizeof (onedig_t)); memcpy (b, y.digit, bl * sizeof (onedig_t)); @@ -1239,10 +1228,10 @@ BigInt::operator%= (BigInt const &y) // Scale as above. But do not copy dividend. It is transformed // into the remainder which is the result we want here. resize (length + 2); - unsigned &al = length; + std::size_t &al = length; onedig_t *a = digit; - unsigned bl = y.length; + std::size_t bl = y.length; onedig_t *b = (onedig_t *)alloca (bl * sizeof (onedig_t)); memcpy (b, y.digit, bl * sizeof (onedig_t)); @@ -1267,10 +1256,9 @@ BigInt::operator%= (BigInt const &y) } // Not part of original BigInt. -unsigned -BigInt::floorPow2 () const +std::size_t BigInt::floorPow2() const { - unsigned i = length; // Start on the last value + std::size_t i = length; // Start on the last value while(i > 0 && digit[i - 1] == 0) { --i; // Skip zeros @@ -1281,7 +1269,7 @@ BigInt::floorPow2 () const } twodig_t power = 1; - unsigned count = 0; + std::size_t count = 0; while((power << 1) <= (twodig_t)digit[i - 1]) { @@ -1292,17 +1280,17 @@ BigInt::floorPow2 () const } // Not part of original BigInt. -void -BigInt::setPower2 (unsigned exponent) { - unsigned digitOffset = exponent / single_bits; - unsigned bitOffset = exponent % single_bits; - unsigned digitsNeeded = 1 + digitOffset; +void BigInt::setPower2(std::size_t exponent) +{ + std::size_t digitOffset = exponent / single_bits; + std::size_t bitOffset = exponent % single_bits; + std::size_t digitsNeeded = 1 + digitOffset; reallocate(digitsNeeded); this->length = digitsNeeded; this->positive = true; - unsigned i; + std::size_t i; for (i = 0; i < digitOffset; ++i) { digit[i] = 0; } diff --git a/src/big-int/bigint.hh b/src/big-int/bigint.hh index 4abaca6abaa..d20808a07a7 100644 --- a/src/big-int/bigint.hh +++ b/src/big-int/bigint.hh @@ -129,15 +129,15 @@ public: enum { small = sizeof (ullong_t) / sizeof (onedig_t) }; private: - unsigned size; // Length of digit vector. - unsigned length; // Used places in digit vector. + std::size_t size; // Length of digit vector. + std::size_t length; // Used places in digit vector. onedig_t *digit; // Least significant first. bool positive; // Signed magnitude representation. // Create or resize this. - inline void allocate (unsigned digits); - inline void reallocate (unsigned digits); - inline void resize (unsigned digits); + inline void allocate(std::size_t digits); + inline void reallocate(std::size_t digits); + inline void resize(std::size_t digits); // Adjust length (e.g. after subtraction). inline void adjust(); @@ -148,12 +148,12 @@ private: // Aux methods, only for internal use. inline int ucompare (BigInt const &) const; - void add (onedig_t const *, unsigned, bool) _fast; - void mul (onedig_t const *, unsigned, bool) _fast; + void add(onedig_t const *, std::size_t, bool) _fast; + void mul(onedig_t const *, std::size_t, bool) _fast; // Auxiliary constructor used for temporary or static BigInt. // Sets size=0 which indicates that ~BigInt must not delete[]. - inline BigInt (onedig_t *, unsigned, bool) _fast; + inline BigInt(onedig_t *, std::size_t, bool) _fast; public: ~BigInt() _fast; @@ -183,19 +183,19 @@ public: // Return an upper bound for the number of digits the textual // representation of this might have. - unsigned digits (onedig_t = 10) const _fast; + std::size_t digits(onedig_t = 10) const _fast; // Convert into string, right adjusted in field of specified width. // Returns pointer to start of number or NULL if field too small. - char *as_string (char *, unsigned, onedig_t = 10) const _fasta; + char *as_string(char *, std::size_t, onedig_t = 10) const _fasta; // Convert to/from a binary representation. // Write and read in a compact byte-wise binary form. Effectively // print in base 256 with the most significant digit first. Also // read back from such a representation. Return success. - bool dump (unsigned char *, unsigned) _fast; - void load (unsigned char const *, unsigned) _fast; + bool dump(unsigned char *, std::size_t) _fast; + void load(unsigned char const *, std::size_t) _fast; // Conversions to elementary types. @@ -275,11 +275,11 @@ public: // Returns the largest x such that 2^x <= abs() or 0 if input is 0 // Not part of original BigInt. - unsigned floorPow2 () const _fast; + std::size_t floorPow2() const _fast; // Sets the number to the power of two given by the exponent // Not part of original BigInt. - void setPower2 (unsigned exponent) _fast; + void setPower2(std::size_t exponent) _fast; void swap (BigInt &other) { @@ -293,7 +293,7 @@ public: // Functions on BigInt. Implementations in bigint-func.cc. -BigInt pow (BigInt const &, unsigned) _fast; +BigInt pow(BigInt const &, std::size_t) _fast; BigInt pow (BigInt const &, BigInt const &, BigInt const &modulus) _fast; BigInt sqrt (BigInt const &) _fast; BigInt gcd (const BigInt &, const BigInt &) _fast; diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index fd0d3c43939..23135e62607 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -102,7 +102,7 @@ const std::string integer2binary(const mp_integer &n, std::size_t width) const std::string integer2string(const mp_integer &n, unsigned base) { - unsigned len = n.digits(base) + 2; + std::size_t len = n.digits(base) + 2; std::vector buffer(len); char *s = n.as_string(buffer.data(), len, base); From f3b2825c68f4e704c1a34485399efbee04d3b810 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:03:04 +0000 Subject: [PATCH 05/18] Explicit casts to avoid conversion warnings: std::size_t Visual Studio warns about signed/unsigned conversion and limited range of types. --- .../java_bytecode_convert_method.cpp | 15 +++++++-------- src/analyses/local_bitvector_analysis.cpp | 6 ++---- src/goto-cc/gcc_cmdline.cpp | 2 +- src/solvers/sat/satcheck_minisat2.cpp | 4 ++-- src/util/string_utils.cpp | 3 ++- src/util/unicode.cpp | 10 +++++----- src/util/unicode.h | 3 ++- src/util/union_find.h | 15 +++++++++------ 8 files changed, 30 insertions(+), 28 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 8d3c23d50f3..109e00ed632 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -825,7 +825,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( { // Range wholly contained within a child block return get_or_create_block_for_pcrange( - tree.branch[child_offset], + tree.branch[static_cast(child_offset)], child_block, address_start, address_limit, @@ -892,7 +892,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( for(auto blockidx=child_offset, blocklim=child_offset+nblocks; blockidx!=blocklim; ++blockidx) - newblock.add(this_block_children[blockidx]); + newblock.add(this_block_children[static_cast(blockidx)]); // Relabel the inner header: to_code_label(newblock.statements()[0]).set_label(new_label_irep); @@ -905,7 +905,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( auto dellim=delfirst; std::advance(dellim, nblocks-1); this_block_children.erase(delfirst, dellim); - this_block_children[child_offset].swap(newlabel); + this_block_children[static_cast(child_offset)].swap(newlabel); // Perform the same transformation on the index tree: block_tree_nodet newnode; @@ -932,14 +932,13 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( ++branchaddriter; tree.branch_addresses.erase(branchaddriter, branchaddrlim); - tree.branch[child_offset]=std::move(newnode); + tree.branch[static_cast(child_offset)] = std::move(newnode); CHECK_RETURN(tree.branch.size() == tree.branch_addresses.size()); - return - to_code_block( - to_code_label( - this_block_children[child_offset]).code()); + return to_code_block( + to_code_label(this_block_children[static_cast(child_offset)]) + .code()); } static void gather_symbol_live_ranges( diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 59d0e110f23..6419eab8148 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -358,10 +358,8 @@ void local_bitvector_analysist::output( p_it!=loc_info.end(); p_it++) { - out << " " << pointers[p_it-loc_info.begin()] - << ": " - << *p_it - << "\n"; + out << " " << pointers[static_cast(p_it - loc_info.begin())] + << ": " << *p_it << "\n"; } out << "\n"; diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp index 46f8fbae0b9..3d54d6ce6c5 100644 --- a/src/goto-cc/gcc_cmdline.cpp +++ b/src/goto-cc/gcc_cmdline.cpp @@ -232,7 +232,7 @@ bool gcc_cmdlinet::parse(int argc, const char **argv) add_arg(argv[0]); argst current_args; - current_args.reserve(argc - 1); + current_args.reserve(static_cast(argc - 1)); for(int i=1; i::l_get(literalt a) const using Minisat::lbool; - if(solver->model[a.var_no()]==l_True) + if(solver->model[static_cast(a.var_no())] == l_True) result=tvt(true); - else if(solver->model[a.var_no()]==l_False) + else if(solver->model[static_cast(a.var_no())] == l_False) result=tvt(false); else return tvt::unknown(); diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 701bfa20ddf..a4659b82a3b 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -33,7 +33,8 @@ std::string strip_string(const std::string &s) =std::find_if_not(s.rbegin(), s.rend(), pred); std::string::size_type j=std::distance(right, s.rend())-1; - return s.substr(i, (j-i+1)); + return s.substr( + static_cast(i), static_cast(j - i + 1)); } void split_string( diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp index ce13365ed49..97219b5a4bb 100644 --- a/src/util/unicode.cpp +++ b/src/util/unicode.cpp @@ -37,7 +37,7 @@ std::string narrow(const wchar_t *s) int slength = static_cast(wcslen(s)); int rlength = WideCharToMultiByte(CP_UTF8, 0, s, slength, NULL, 0, NULL, NULL); - std::string r(rlength, 0); + std::string r(static_cast(rlength), 0); WideCharToMultiByte(CP_UTF8, 0, s, slength, &r[0], rlength, NULL, NULL); return r; @@ -52,7 +52,7 @@ std::wstring widen(const char *s) int slength = static_cast(strlen(s)); int rlength = MultiByteToWideChar(CP_UTF8, 0, s, slength, NULL, 0); - std::wstring r(rlength, 0); + std::wstring r(static_cast(rlength), 0); MultiByteToWideChar(CP_UTF8, 0, s, slength, &r[0], rlength); return r; @@ -68,7 +68,7 @@ std::string narrow(const std::wstring &s) int slength = static_cast(s.size()); int rlength = WideCharToMultiByte(CP_UTF8, 0, &s[0], slength, NULL, 0, NULL, NULL); - std::string r(rlength, 0); + std::string r(static_cast(rlength), 0); WideCharToMultiByte(CP_UTF8, 0, &s[0], slength, &r[0], rlength, NULL, NULL); return r; @@ -90,7 +90,7 @@ std::wstring widen(const std::string &s) int slength = static_cast(s.size()); int rlength = MultiByteToWideChar(CP_UTF8, 0, &s[0], slength, NULL, 0); - std::wstring r(rlength, 0); + std::wstring r(static_cast(rlength), 0); MultiByteToWideChar(CP_UTF8, 0, &s[0], slength, &r[0], rlength); return r; @@ -151,7 +151,7 @@ std::vector narrow_argv(int argc, const wchar_t **argv_wide) return std::vector(); std::vector argv_narrow; - argv_narrow.reserve(argc); + argv_narrow.reserve(static_cast(argc)); for(int i = 0; i != argc; ++i) argv_narrow.push_back(narrow(argv_wide[i])); diff --git a/src/util/unicode.h b/src/util/unicode.h index 327b3093d1b..929d0c1f2ce 100644 --- a/src/util/unicode.h +++ b/src/util/unicode.h @@ -65,7 +65,8 @@ template std::vector to_c_str_array(It b, It e) { // Assumes that walking the range will be faster than repeated allocation - std::vector ret(std::distance(b, e) + 1, nullptr); + std::vector ret( + static_cast(std::distance(b, e) + 1), nullptr); std::transform( b, e, std::begin(ret), [](const std::string &s) { return s.c_str(); }); return ret; diff --git a/src/util/union_find.h b/src/util/union_find.h index f38a7e99022..80a5f2e3c7b 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -163,7 +163,8 @@ class union_find final // true == already in same set bool make_union(const_iterator it_a, const_iterator it_b) { - size_type na=it_a-numbers.begin(), nb=it_b-numbers.begin(); + size_type na = static_cast(it_a - numbers.begin()), + nb = static_cast(it_b - numbers.begin()); bool is_union=find_number(na)==find_number(nb); uuf.make_union(na, nb); return is_union; @@ -185,12 +186,14 @@ class union_find final // are 'a' and 'b' in the same set? bool same_set(const_iterator it_a, const_iterator it_b) const { - return uuf.same_set(it_a-numbers.begin(), it_b-numbers.begin()); + return uuf.same_set( + static_cast(it_a - numbers.begin()), + static_cast(it_b - numbers.begin())); } const T &find(const_iterator it) const { - return numbers[find_number(it-numbers.begin())]; + return numbers[find_number(static_cast(it - numbers.begin()))]; } const T &find(const T &a) @@ -200,7 +203,7 @@ class union_find final size_type find_number(const_iterator it) const { - return find_number(it-numbers.begin()); + return find_number(static_cast(it - numbers.begin())); } size_type find_number(size_type a) const @@ -229,7 +232,7 @@ class union_find final bool is_root(const_iterator it) const { - return uuf.is_root(it-numbers.begin()); + return uuf.is_root(static_cast(it - numbers.begin())); } size_type number(const T &a) @@ -252,7 +255,7 @@ class union_find final void isolate(const_iterator it) { - uuf.isolate(it-numbers.begin()); + uuf.isolate(static_cast(it - numbers.begin())); } void isolate(const T &a) From e5f0b024597b989de93203f7e8405b42c8666c03 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:06:04 +0000 Subject: [PATCH 06/18] Explicitly cast returnvalue of tolower to char Visual Studio warns about signed/unsigned conversion and limited range of types. --- jbmc/src/java_bytecode/java_types.cpp | 2 +- src/ansi-c/literals/parse_float.cpp | 6 ++++-- src/goto-cc/goto_cc_main.cpp | 9 ++++++--- src/goto-cc/ms_link_cmdline.cpp | 4 +++- src/goto-programs/interpreter.cpp | 12 ++++++------ 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index d6f2c1b9ffe..b4c8dda2dc2 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -656,7 +656,7 @@ std::optional java_type_from_string( subtype_letter=='[' || // Array-of-arrays subtype_letter=='T') // Array of generic types subtype_letter='A'; - subtype_letter = std::tolower(subtype_letter); + subtype_letter = static_cast(std::tolower(subtype_letter)); if(subtype_letter == 'a') { return java_reference_array_type( diff --git a/src/ansi-c/literals/parse_float.cpp b/src/ansi-c/literals/parse_float.cpp index bd0fc35d144..7a03a7822f1 100644 --- a/src/ansi-c/literals/parse_float.cpp +++ b/src/ansi-c/literals/parse_float.cpp @@ -30,8 +30,10 @@ parse_floatt::parse_floatt(const std::string &src) // by first converting to lower case. std::string src_lower=src; - std::transform(src_lower.begin(), src_lower.end(), - src_lower.begin(), ::tolower); + std::transform( + src_lower.begin(), src_lower.end(), src_lower.begin(), [](char c) { + return static_cast(std::tolower(c)); + }); const char *p=src_lower.c_str(); diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-cc/goto_cc_main.cpp index 45ce938e81b..03b285d0453 100644 --- a/src/goto-cc/goto_cc_main.cpp +++ b/src/goto-cc/goto_cc_main.cpp @@ -11,11 +11,12 @@ Date: May 2006 /// \file /// GOTO-CC Main Module +#include + #include +#include #include -#include - #ifdef _MSC_VER # include #endif @@ -40,7 +41,9 @@ Date: May 2006 std::string to_lower_string(const std::string &s) { std::string result=s; - transform(result.begin(), result.end(), result.begin(), tolower); + transform(result.begin(), result.end(), result.begin(), [](char c) { + return static_cast(std::tolower(c)); + }); return result; } diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp index ddf5ae3d8c1..bbb9a3348c1 100644 --- a/src/goto-cc/ms_link_cmdline.cpp +++ b/src/goto-cc/ms_link_cmdline.cpp @@ -313,7 +313,9 @@ const char *ms_link_options[] = { static std::string to_upper_string(const std::string &s) { std::string result = s; - transform(result.begin(), result.end(), result.begin(), toupper); + transform(result.begin(), result.end(), result.begin(), [](char c) { + return static_cast(std::toupper(c)); + }); return result; } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 8ad54ddbf2d..7cf52e5346a 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -136,7 +136,7 @@ void interpretert::command() return; } - char ch=tolower(command[0]); + char ch = static_cast(tolower(static_cast(command[0]))); if(ch=='q') done=true; else if(ch=='h') @@ -158,7 +158,7 @@ void interpretert::command() { json_arrayt json_steps; convert(ns, steps, json_steps); - ch=tolower(command[1]); + ch = static_cast(tolower(command[1])); if(ch==' ') { std::ofstream file; @@ -174,12 +174,12 @@ void interpretert::command() } else if(ch=='m') { - ch=tolower(command[1]); + ch = static_cast(tolower(command[1])); print_memory(ch=='i'); } else if(ch=='o') { - ch=tolower(command[1]); + ch = static_cast(tolower(command[1])); if(ch==' ') { std::ofstream file; @@ -195,14 +195,14 @@ void interpretert::command() } else if(ch=='r') { - ch=tolower(command[1]); + ch = static_cast(tolower(command[1])); initialize(ch!='0'); } else if((ch=='s') || (ch==0)) { num_steps=1; std::size_t stack_depth = npos; - ch=tolower(command[1]); + ch = static_cast(tolower(command[1])); if(ch=='e') num_steps=npos; else if(ch=='o') From 5db89ef9e9eabc9fb55bd6cdb7a83a5b2e92dbc1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:07:22 +0000 Subject: [PATCH 07/18] std::distance returns a signed type, wrap in explicit cast Visual Studio warns about signed/unsigned conversion and limited range of types. --- .../pointer-analysis/custom_value_set_analysis.cpp | 2 +- src/cpp/cpp_token_buffer.cpp | 5 +++-- src/goto-instrument/goto_program2code.cpp | 11 +++++++---- src/solvers/flattening/boolbv_complex.cpp | 2 +- src/solvers/flattening/boolbv_extractbits.cpp | 4 +++- src/solvers/flattening/boolbv_mult.cpp | 3 ++- src/solvers/flattening/boolbv_typecast.cpp | 6 ++++-- src/solvers/flattening/boolbv_unary_minus.cpp | 3 ++- src/solvers/flattening/bv_utils.cpp | 7 +++++-- src/solvers/floatbv/float_utils.cpp | 10 +++++++--- src/util/simplify_expr_int.cpp | 6 ++++-- src/util/string_utils.cpp | 4 ++-- 12 files changed, 41 insertions(+), 22 deletions(-) diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 85d255eb5a8..05d46cd397d 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -147,7 +147,7 @@ typedef #define TEST_FUNCTION_NAME TEST_PREFIX "test:()V" #define TEST_LOCAL_PREFIX TEST_FUNCTION_NAME "::" -static std::size_t +static std::ptrdiff_t exprs_with_id(const std::vector &exprs, const irep_idt &id) { return std::count_if( diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp index d5c97e731d4..dbb79e0d5ea 100644 --- a/src/cpp/cpp_token_buffer.cpp +++ b/src/cpp/cpp_token_buffer.cpp @@ -119,6 +119,7 @@ void cpp_token_buffert::Insert(const cpp_tokent &token) tokens.push_back(token); - token_vector.insert(token_vector.begin()+current_pos, - --tokens.end()); + token_vector.insert( + token_vector.begin() + static_cast(current_pos), + --tokens.end()); } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 87edc71b678..7381dfd302f 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1559,7 +1559,8 @@ void goto_program2codet::cleanup_code_block( operands.size()>1 && i(i); // remove skip if(to_code(*it).get_statement()==ID_skip && it->source_location().get_comment().empty()) @@ -1579,9 +1580,11 @@ void goto_program2codet::cleanup_code_block( if(!has_decl) { - operands.insert(operands.begin()+i+1, - it->operands().begin(), it->operands().end()); - operands.erase(operands.begin()+i); + operands.insert( + operands.begin() + static_cast(i) + 1, + it->operands().begin(), + it->operands().end()); + operands.erase(operands.begin() + static_cast(i)); // no ++i } else diff --git a/src/solvers/flattening/boolbv_complex.cpp b/src/solvers/flattening/boolbv_complex.cpp index e448e393ddd..d0d80fbad7f 100644 --- a/src/solvers/flattening/boolbv_complex.cpp +++ b/src/solvers/flattening/boolbv_complex.cpp @@ -51,7 +51,7 @@ bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr) bvt bv = convert_bv(expr.op(), width * 2); - bv.erase(bv.begin(), bv.begin()+width); + bv.erase(bv.begin(), bv.begin() + static_cast(width)); return bv; } diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 566d030606d..886199d585e 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -40,7 +40,9 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) const std::size_t offset = numeric_cast_v(index_as_int); - bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width); + bvt result_bv( + src_bv.begin() + static_cast(offset), + src_bv.begin() + static_cast(offset + bv_width)); return result_bv; } diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp index 2d94e54df4f..452fc29c839 100644 --- a/src/solvers/flattening/boolbv_mult.cpp +++ b/src/solvers/flattening/boolbv_mult.cpp @@ -50,7 +50,8 @@ bvt boolbvt::convert_mult(const mult_exprt &expr) bv=bv_utils.signed_multiplier(bv, op); // cut it down again - bv.erase(bv.begin(), bv.begin()+fraction_bits); + bv.erase( + bv.begin(), bv.begin() + static_cast(fraction_bits)); } return bv; diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 84d25cc8883..e74854d35fb 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -77,8 +77,10 @@ bool boolbvt::type_conversion( { // recursively do both halfs bvt lower, upper, lower_res, upper_res; - lower.assign(src.begin(), src.begin() + src.size() / 2); - upper.assign(src.begin() + src.size() / 2, src.end()); + lower.assign( + src.begin(), src.begin() + static_cast(src.size() / 2)); + upper.assign( + src.begin() + static_cast(src.size() / 2), src.end()); type_conversion( to_complex_type(src_type).subtype(), lower, diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp index 5df1699c7a4..bf8246790f4 100644 --- a/src/solvers/flattening/boolbv_unary_minus.cpp +++ b/src/solvers/flattening/boolbv_unary_minus.cpp @@ -51,7 +51,8 @@ bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr) { bvt tmp_op; - const auto sub_it = std::next(op_bv.begin(), sub_idx); + const auto sub_it = + std::next(op_bv.begin(), static_cast(sub_idx)); std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op)); if(subtype.id() == ID_floatbv) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 31dd12fea20..d27f085316b 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -48,7 +48,8 @@ bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last) bvt result=a; result.resize(last+1); if(first!=0) - result.erase(result.begin(), result.begin()+first); + result.erase( + result.begin(), result.begin() + static_cast(first)); POSTCONDITION(result.size() == last - first + 1); return result; @@ -60,7 +61,9 @@ bvt bv_utilst::extract_msb(const bvt &a, std::size_t n) PRECONDITION(n <= a.size()); bvt result=a; - result.erase(result.begin(), result.begin()+(result.size()-n)); + result.erase( + result.begin(), + result.begin() + static_cast(result.size() - n)); POSTCONDITION(result.size() == n); return result; diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp index dc94a842226..d9d9fb19cda 100644 --- a/src/solvers/floatbv/float_utils.cpp +++ b/src/solvers/floatbv/float_utils.cpp @@ -393,7 +393,9 @@ bvt float_utilst::limit_distance( std::size_t nb_bits = address_bits(limit); bvt upper_bits=dist; - upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits); + upper_bits.erase( + upper_bits.begin(), + upper_bits.begin() + static_cast(nb_bits)); literalt or_upper_bits=prop.lor(upper_bits); bvt lower_bits=dist; @@ -713,7 +715,8 @@ literalt float_utilst::exponent_all_ones(const bvt &src) bvt exponent=src; // removes the fractional part - exponent.erase(exponent.begin(), exponent.begin()+spec.f); + exponent.erase( + exponent.begin(), exponent.begin() + static_cast(spec.f)); // removes the sign exponent.resize(spec.e); @@ -726,7 +729,8 @@ literalt float_utilst::exponent_all_zeros(const bvt &src) bvt exponent=src; // removes the fractional part - exponent.erase(exponent.begin(), exponent.begin()+spec.f); + exponent.erase( + exponent.begin(), exponent.begin() + static_cast(spec.f)); // removes the sign exponent.resize(spec.e); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 97fb7242e1e..6ef0680d329 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -949,7 +949,8 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) else opi = eb_merged; // erase opn - new_expr.operands().erase(new_expr.operands().begin() + i + 1); + new_expr.operands().erase( + new_expr.operands().begin() + static_cast(i) + 1); no_change = false; } else @@ -981,7 +982,8 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) to_bitvector_type(opi.type()).set_width(new_value.size()); opi.type().id(ID_verilog_unsignedbv); // erase opn - new_expr.operands().erase(new_expr.operands().begin() + i + 1); + new_expr.operands().erase( + new_expr.operands().begin() + static_cast(i) + 1); no_change = false; } else diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index a4659b82a3b..ecded0a3a80 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -27,11 +27,11 @@ std::string strip_string(const std::string &s) if(left==s.end()) return ""; - std::string::size_type i=std::distance(s.begin(), left); + const auto i = std::distance(s.begin(), left); std::string::const_reverse_iterator right =std::find_if_not(s.rbegin(), s.rend(), pred); - std::string::size_type j=std::distance(right, s.rend())-1; + const auto j = std::distance(right, s.rend()) - 1; return s.substr( static_cast(i), static_cast(j - i + 1)); From 86f73d8fc596cecd0fb3a5f6d3d69b293d933b45 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:08:26 +0000 Subject: [PATCH 08/18] Explicit casts to avoid conversion warnings Visual Studio warns about signed/unsigned conversion and limited range of types. --- src/ansi-c/expr2c.cpp | 2 +- src/ansi-c/literals/convert_string_literal.cpp | 6 +++--- src/ansi-c/literals/unescape_string.cpp | 10 +++++----- src/goto-checker/symex_coverage.cpp | 3 ++- src/goto-programs/elf_reader.cpp | 6 ++++-- src/goto-programs/elf_reader.h | 11 ++++++++--- src/goto-programs/read_bin_goto_object.cpp | 3 ++- src/goto-programs/read_goto_binary.cpp | 2 +- src/solvers/floatbv/float_bv.cpp | 2 +- src/solvers/floatbv/float_utils.cpp | 2 +- src/solvers/sat/cnf.cpp | 2 +- src/solvers/sat/satcheck_minisat2.cpp | 6 +++--- src/solvers/smt2/smt2_conv.cpp | 2 +- .../strings/string_constraint_generator_float.cpp | 2 +- src/util/arith_tools.cpp | 3 ++- src/util/irep_hash.h | 3 ++- src/util/irep_serialization.cpp | 2 +- src/util/run.cpp | 2 +- src/util/small_map.h | 2 +- src/util/string_container.cpp | 4 ++-- src/util/tempfile.cpp | 2 +- src/util/xml.cpp | 3 ++- 22 files changed, 46 insertions(+), 34 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6a390a2100f..e0501c716fc 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2233,7 +2233,7 @@ std::string expr2ct::convert_array(const exprt &src) if(last_was_hex) { // we use "string splicing" to avoid ambiguity - if(isxdigit(ch)) + if(isxdigit(static_cast(ch))) dest+="\" \""; last_was_hex=false; diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp index 381bb38f95e..e5d0689f673 100644 --- a/src/ansi-c/literals/convert_string_literal.cpp +++ b/src/ansi-c/literals/convert_string_literal.cpp @@ -36,7 +36,7 @@ std::basic_string convert_one_string_literal(const std::string &src) // pad into wide string value.resize(utf8_value.size()); for(std::size_t i=0; i(utf8_value[i]); return value; } @@ -59,7 +59,7 @@ std::basic_string convert_one_string_literal(const std::string &src) std::basic_string value; value.resize(char_value.size()); for(std::size_t i=0; i(char_value[i]); return value; } @@ -143,7 +143,7 @@ exprt convert_string_literal(const std::string &src) { // Loss of data here if value[i]>255. // gcc issues a warning in this case. - char_value[i]=value[i]; + char_value[i] = static_cast(value[i]); } return string_constantt(char_value); diff --git a/src/ansi-c/literals/unescape_string.cpp b/src/ansi-c/literals/unescape_string.cpp index b8c1dbcea94..f3b534c4ea9 100644 --- a/src/ansi-c/literals/unescape_string.cpp +++ b/src/ansi-c/literals/unescape_string.cpp @@ -43,7 +43,7 @@ std::basic_string unescape_string_templ(const std::string &src) for(unsigned i=0; i(static_cast(src[i])); if(ch=='\\') // escape? { @@ -51,7 +51,7 @@ std::basic_string unescape_string_templ(const std::string &src) i++; INVARIANT(i < src.size(), "backslash can't be last character"); - ch=(unsigned char)src[i]; + ch = static_cast(static_cast(src[i])); switch(ch) { case '\\': dest.push_back(ch); break; @@ -105,7 +105,7 @@ std::basic_string unescape_string_templ(const std::string &src) // go back i--; - ch=hex_to_unsigned(hex.c_str(), hex.size()); + ch = static_cast(hex_to_unsigned(hex.c_str(), hex.size())); } // if T isn't sufficiently wide to hold unsigned values @@ -116,7 +116,7 @@ std::basic_string unescape_string_templ(const std::string &src) break; default: - if(isdigit(ch)) // octal + if(isdigit(static_cast(ch))) // octal { std::string octal; @@ -129,7 +129,7 @@ std::basic_string unescape_string_templ(const std::string &src) // go back i--; - ch=octal_to_unsigned(octal.c_str(), octal.size()); + ch = static_cast(octal_to_unsigned(octal.c_str(), octal.size())); dest.push_back(ch); } else diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp index 6e4edbe81d3..6d2b2bb1600 100644 --- a/src/goto-checker/symex_coverage.cpp +++ b/src/goto-checker/symex_coverage.cpp @@ -194,7 +194,8 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( xmlt &condition = conditions.new_element("condition"); condition.set_attribute("number", std::to_string(number++)); condition.set_attribute("type", "jump"); - unsigned taken = c.second.false_taken + c.second.true_taken; + unsigned taken = + static_cast(c.second.false_taken + c.second.true_taken); total_taken += taken; condition.set_attribute("coverage", rate(taken, 2, true)); } diff --git a/src/goto-programs/elf_reader.cpp b/src/goto-programs/elf_reader.cpp index 10ecb30085c..c7bfc6b7d6f 100644 --- a/src/goto-programs/elf_reader.cpp +++ b/src/goto-programs/elf_reader.cpp @@ -107,7 +107,8 @@ elf_readert::elf_readert(std::istream &_in):in(_in) for(std::size_t i=0; i( + elf32_header.e_shoff + i * elf32_header.e_shentsize)); // read section header in.read( @@ -187,7 +188,8 @@ elf_readert::elf_readert(std::istream &_in):in(_in) for(std::size_t i=0; i( + elf64_header.e_shoff + i * elf64_header.e_shentsize)); // read section header in.read( diff --git a/src/goto-programs/elf_reader.h b/src/goto-programs/elf_reader.h index f3014fad5e3..94bb23ba488 100644 --- a/src/goto-programs/elf_reader.h +++ b/src/goto-programs/elf_reader.h @@ -143,9 +143,14 @@ class elf_readert std::streampos section_offset(std::size_t index) const { - return - elf_class==ELF32?elf32_section_header_table[index].sh_offset: - elf64_section_header_table[index].sh_offset; + // Visual Studio insists on a type cast to std::streamoff, for an unknown + // reason + if(elf_class == ELF32) + return static_cast( + elf32_section_header_table[index].sh_offset); + else + return static_cast( + elf64_section_header_table[index].sh_offset); } bool has_section(const std::string &name) const; diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index bf758f2c4b4..208ccffe13f 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -146,7 +146,8 @@ static void read_bin_functions_object( std::size_t t_count = irepconverter.read_gb_word(in); // # of targets for(std::size_t i=0; i(irepconverter.read_gb_word(in))); std::size_t l_count = irepconverter.read_gb_word(in); // # of labels diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 89b07a92a99..b2316ecd51d 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -98,7 +98,7 @@ static bool read_goto_binary( for(unsigned i=0; i(elf_reader.section_offset(i))); return read_bin_goto_object( in, filename, symbol_table, goto_functions, message_handler); } diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 9450694fb43..19531430d21 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -426,7 +426,7 @@ exprt float_bvt::conversion( int sourceSmallestNormalExponent = -((1 << (src_spec.e - 1)) - 1); int sourceSmallestDenormalExponent = - sourceSmallestNormalExponent - src_spec.f; + sourceSmallestNormalExponent - static_cast(src_spec.f); // Using the fact that f doesn't include the hidden bit diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp index d9d9fb19cda..9e8389e627a 100644 --- a/src/solvers/floatbv/float_utils.cpp +++ b/src/solvers/floatbv/float_utils.cpp @@ -168,7 +168,7 @@ bvt float_utilst::conversion( int sourceSmallestNormalExponent=-((1 << (spec.e - 1)) - 1); int sourceSmallestDenormalExponent = - sourceSmallestNormalExponent - spec.f; + sourceSmallestNormalExponent - static_cast(spec.f); // Using the fact that f doesn't include the hidden bit diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp index d15e301711a..5fe9067ea57 100644 --- a/src/solvers/sat/cnf.cpp +++ b/src/solvers/sat/cnf.cpp @@ -384,7 +384,7 @@ literalt cnft::lselect(literalt a, literalt b, literalt c) /// \return New variable as literal literalt cnft::new_variable() { - literalt l(_no_variables, false); + literalt l(static_cast(_no_variables), false); set_no_variables(_no_variables+1); diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 266c537cf1e..633d4f1ff8a 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -309,7 +309,7 @@ void satcheck_minisat2_baset::set_assignment(literalt a, bool value) try { - unsigned v = a.var_no(); + unsigned v = static_cast(a.var_no()); bool sign = a.sign(); // MiniSat2 kills the model in case of UNSAT @@ -359,7 +359,7 @@ void satcheck_minisat_simplifiert::set_frozen(literalt a) if(!a.is_constant()) { add_variables(); - solver->setFrozen(a.var_no(), true); + solver->setFrozen(static_cast(a.var_no()), true); } } catch(const Minisat::OutOfMemoryException &) @@ -374,5 +374,5 @@ bool satcheck_minisat_simplifiert::is_eliminated(literalt a) const { PRECONDITION(!a.is_constant()); - return solver->isEliminated(a.var_no()); + return solver->isEliminated(static_cast(a.var_no())); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 7880119ab7d..353908c09be 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -917,7 +917,7 @@ literalt smt2_convt::convert(const exprt &expr) exprt prepared_expr = prepare_for_convert_expr(expr); - literalt l(no_boolean_variables, false); + literalt l(static_cast(no_boolean_variables), false); no_boolean_variables++; out << "; convert\n"; diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp index e33c5794a51..9d15325a486 100644 --- a/src/solvers/strings/string_constraint_generator_float.cpp +++ b/src/solvers/strings/string_constraint_generator_float.cpp @@ -79,7 +79,7 @@ exprt constant_float(const double f, const ieee_float_spect &float_spec) { ieee_float_valuet fl(float_spec); if(float_spec == ieee_float_spect::single_precision()) - fl.from_float(f); + fl.from_float(static_cast(f)); else if(float_spec == ieee_float_spect::double_precision()) fl.from_double(f); else diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 7d40b77b60d..15e08368098 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -290,7 +290,8 @@ bool get_bvrep_bit( "bvrep is hexadecimal, upper-case"); const unsigned char nibble_value = - isdigit(nibble) ? nibble - '0' : nibble - 'A' + 10; + isdigit(nibble) ? static_cast(nibble - '0') + : static_cast(nibble - 'A' + 10); return ((nibble_value >> (bit_index % 4)) & 1) != 0; } diff --git a/src/util/irep_hash.h b/src/util/irep_hash.h index 0d5962a221d..aed5fc8fe15 100644 --- a/src/util/irep_hash.h +++ b/src/util/irep_hash.h @@ -83,7 +83,8 @@ inline std::size_t basic_hash_combine<32>( std::size_t h1, std::size_t h2) { - return ROTL32(h1, 7)^h2; + return static_cast( + ROTL32(static_cast(h1), 7) ^ static_cast(h2)); } template<> diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index 20f37d8a194..66576c307f4 100644 --- a/src/util/irep_serialization.cpp +++ b/src/util/irep_serialization.cpp @@ -129,7 +129,7 @@ void write_gb_word(std::ostream &out, std::size_t u) if(u==0) { - out.put(value); + out.put(static_cast(value)); break; } diff --git a/src/util/run.cpp b/src/util/run.cpp index 2597dc5c14e..872bc02b21b 100644 --- a/src/util/run.cpp +++ b/src/util/run.cpp @@ -342,7 +342,7 @@ int run( CloseHandle(piProcInfo.hProcess); CloseHandle(piProcInfo.hThread); - return exit_code; + return static_cast(exit_code); #else int stdin_fd = stdio_redirection(STDIN_FILENO, std_input); diff --git a/src/util/small_map.h b/src/util/small_map.h index e367e08769c..438ba82b5c9 100644 --- a/src/util/small_map.h +++ b/src/util/small_map.h @@ -389,7 +389,7 @@ class small_mapt const_value_iterator value_begin() const { - return const_value_iterator(*this, size() - 1); + return const_value_iterator(*this, static_cast(size()) - 1); } const_value_iterator value_end() const diff --git a/src/util/string_container.cpp b/src/util/string_container.cpp index bc81c861409..8c1b23d9a94 100644 --- a/src/util/string_container.cpp +++ b/src/util/string_container.cpp @@ -40,7 +40,7 @@ unsigned string_containert::get(const char *s) if(it!=hash_table.end()) return it->second; - size_t r=hash_table.size(); + const unsigned r = static_cast(hash_table.size()); // these are stable string_list.push_back(std::string(s)); @@ -63,7 +63,7 @@ unsigned string_containert::get(const std::string &s) if(it!=hash_table.end()) return it->second; - size_t r=hash_table.size(); + const unsigned r = static_cast(hash_table.size()); // these are stable string_list.push_back(s); diff --git a/src/util/tempfile.cpp b/src/util/tempfile.cpp index ad0e6dec577..aebcd0412e5 100644 --- a/src/util/tempfile.cpp +++ b/src/util/tempfile.cpp @@ -130,7 +130,7 @@ std::string get_temporary_file( char *t_ptr=strdup(t_template.c_str()); - int fd=mkstemps(t_ptr, suffix.size()); + int fd = mkstemps(t_ptr, static_cast(suffix.size())); if(fd<0) throw system_exceptiont("Failed to open temporary file"); diff --git a/src/util/xml.cpp b/src/util/xml.cpp index 803037b68a1..4c718c6b50a 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -260,7 +260,8 @@ std::string xmlt::unescape(const std::string &str) result+='&'; else if(tmp[0]=='#' && tmp[1]!='x') { - char c=unsafe_string2int(tmp.substr(1, tmp.size()-1)); + char c = + static_cast(unsafe_string2int(tmp.substr(1, tmp.size() - 1))); result+=c; } else From 86f51f9e52eb532591f207b0520705df68db3385 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:10:11 +0000 Subject: [PATCH 09/18] Explicit casts to avoid conversion warnings: irept::set takes a signed long long Visual Studio warns about signed/unsigned conversion and limited range of types. --- src/cpp/cpp_convert_type.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index d55fd811898..b8bb8f18867 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -335,7 +335,7 @@ void cpp_convert_plain_type(typet &type, message_handlert &message_handler) } else if(type.id() == ID_c_bool) { - type.set(ID_width, config.ansi_c.bool_width); + type.set(ID_width, static_cast(config.ansi_c.bool_width)); } else { From 189537538c048ead0bf98f786b673967d7e3c57c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jan 2019 16:27:21 +0000 Subject: [PATCH 10/18] Use auto where type does not matter (and is likely signed) This avoids conversion warnings with Visual Studio. --- .../virtual_call_null_checks.cpp | 9 ++++----- unit/util/irep.cpp | 2 +- unit/util/range.cpp | 3 +-- 3 files changed, 6 insertions(+), 8 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp index 18ec6f3747a..bf5f8cbcf7d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp @@ -60,11 +60,10 @@ SCENARIO( { // This just checks that the class actually makes the expected call, // i.e. that it hasn't been optimised away or similar. - std::size_t found_virtualmethod_calls = - std::count_if( - main_function.body.instructions.begin(), - main_function.body.instructions.end(), - is_expected_virtualmethod_call); + auto found_virtualmethod_calls = std::count_if( + main_function.body.instructions.begin(), + main_function.body.instructions.end(), + is_expected_virtualmethod_call); REQUIRE(found_virtualmethod_calls == 1); } diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index 66f92ffd63c..9cc769746b5 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -148,7 +148,7 @@ SCENARIO("irept_memory", "[core][utils][irept]") irep.add("a_new_element", irep2); REQUIRE(!irept::is_comment("a_new_element")); REQUIRE(irep.find("a_new_element").id() == "second_irep"); - std::size_t named_sub_size = + auto named_sub_size = std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end()); REQUIRE(named_sub_size == 1); diff --git a/unit/util/range.cpp b/unit/util/range.cpp index 4c63bae3ff3..15d3cd2e573 100644 --- a/unit/util/range.cpp +++ b/unit/util/range.cpp @@ -406,8 +406,7 @@ SCENARIO( THEN("A range of made from the vector can be filtered.") { const auto odds_filter = make_range(input).filter(is_odd); - const std::size_t total = - std::distance(odds_filter.begin(), odds_filter.end()); + const auto total = std::distance(odds_filter.begin(), odds_filter.end()); REQUIRE(total == 5); auto iterator = odds_filter.begin(); REQUIRE((iterator++)->value == 1); From 247f81ab5f08c012576667983e2193d6973e6e01 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jun 2018 17:51:18 +0000 Subject: [PATCH 11/18] Use std::size_t when referring to object size --- jbmc/src/java_bytecode/java_bmc_util.cpp | 6 +- .../java_enum_static_init_unwind_handler.cpp | 6 +- .../java_enum_static_init_unwind_handler.h | 6 +- .../java_local_variable_table.cpp | 6 +- src/analyses/custom_bitvector_analysis.cpp | 20 +++--- src/analyses/custom_bitvector_analysis.h | 12 ++-- src/analyses/invariant_propagation.h | 2 +- src/analyses/invariant_set.cpp | 62 +++++++++---------- src/analyses/invariant_set.h | 60 +++++++++--------- src/analyses/local_may_alias.cpp | 14 ++--- src/analyses/local_may_alias.h | 4 +- src/ansi-c/ansi_c_typecheck.cpp | 2 +- .../literals/convert_integer_literal.cpp | 2 +- src/cpp/cpp_token_buffer.cpp | 4 +- src/cpp/cpp_token_buffer.h | 6 +- src/cpp/cpp_typecheck.cpp | 2 +- src/cpp/parse.cpp | 24 +++---- src/goto-cc/compile.cpp | 2 +- src/goto-checker/symex_bmc.cpp | 14 ++--- src/goto-checker/symex_bmc.h | 10 +-- .../symex_bmc_incremental_one_loop.h | 10 +-- src/goto-instrument/accelerate/accelerate.cpp | 14 ++--- .../accelerate/acceleration_utils.cpp | 10 ++- .../accelerate/all_paths_enumerator.cpp | 10 +-- .../accelerate/all_paths_enumerator.h | 6 +- src/goto-instrument/accelerate/polynomial.cpp | 12 ++-- src/goto-instrument/accelerate/polynomial.h | 6 +- .../accelerate/trace_automaton.cpp | 6 +- .../accelerate/trace_automaton.h | 2 +- src/goto-instrument/cover_instrument_mcdc.cpp | 2 +- src/goto-instrument/document_properties.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 8 ++- src/goto-instrument/unwindset.cpp | 10 +-- src/goto-instrument/unwindset.h | 4 +- src/goto-instrument/wmm/data_dp.cpp | 2 +- src/goto-instrument/wmm/goto2graph.cpp | 4 +- src/goto-instrument/wmm/goto2graph.h | 2 +- src/goto-instrument/wmm/weak_memory.cpp | 6 +- src/goto-programs/goto_trace.cpp | 4 +- src/goto-programs/goto_trace.h | 2 +- src/goto-programs/structured_trace_util.h | 2 +- src/goto-programs/write_goto_binary.cpp | 4 +- src/goto-programs/write_goto_binary.h | 6 +- src/goto-symex/complexity_limiter.cpp | 6 +- src/goto-symex/goto_symex.h | 6 +- src/goto-symex/goto_symex_state.h | 2 +- src/goto-symex/memory_model.h | 2 +- src/goto-symex/partial_order_concurrency.cpp | 4 +- src/goto-symex/renaming_level.cpp | 2 +- src/goto-symex/renaming_level.h | 2 +- src/goto-symex/symex_function_call.cpp | 5 +- src/goto-symex/symex_goto.cpp | 18 +++--- src/goto-symex/symex_main.cpp | 4 +- src/goto-symex/symex_target.h | 2 +- src/pointer-analysis/value_set.cpp | 2 +- src/pointer-analysis/value_set_fi.h | 10 +-- src/solvers/bdd/miniBDD/miniBDD.cpp | 32 +++++----- src/solvers/bdd/miniBDD/miniBDD.h | 27 ++++---- src/solvers/bdd/miniBDD/miniBDD.inc | 25 +++++--- src/solvers/flattening/equality.cpp | 6 +- src/solvers/flattening/equality.h | 6 +- src/solvers/floatbv/float_approximation.cpp | 9 +-- src/solvers/floatbv/float_approximation.h | 2 +- src/solvers/floatbv/float_bv.cpp | 15 ++--- src/solvers/floatbv/float_utils.cpp | 9 +-- src/solvers/prop/cover_goals.h | 4 +- src/solvers/qbf/qbf_qube_core.h | 2 +- src/solvers/refinement/bv_refinement_loop.cpp | 6 +- src/solvers/refinement/refine_arrays.cpp | 2 +- src/solvers/smt2/smt2_parser.cpp | 11 ++-- .../strings/string_constraint_generator.h | 4 +- .../string_constraint_generator_valueof.cpp | 28 ++++----- src/util/graph.h | 19 +++--- src/util/string_expr.h | 2 +- src/util/typecheck.cpp | 2 +- src/xmllang/scanner.l | 2 +- unit/analyses/call_graph.cpp | 4 +- unit/solvers/bdd/miniBDD/miniBDD.cpp | 2 +- unit/util/format_number_range.cpp | 2 +- unit/util/small_map.cpp | 6 +- 80 files changed, 344 insertions(+), 346 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bmc_util.cpp b/jbmc/src/java_bytecode/java_bmc_util.cpp index dbe3ed8f2a2..2b8e2641136 100644 --- a/jbmc/src/java_bytecode/java_bmc_util.cpp +++ b/jbmc/src/java_bytecode/java_bmc_util.cpp @@ -29,9 +29,9 @@ void java_setup_symex( symex.add_loop_unwind_handler( [&goto_model]( const call_stackt &context, - unsigned loop_num, - unsigned unwind, - unsigned &max_unwind) + std::size_t loop_num, + std::size_t unwind, + std::size_t &max_unwind) { // NOLINT (*) return java_enum_static_init_unwind_handler( context, loop_num, unwind, max_unwind, goto_model.get_symbol_table()); diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp index bd89b07e2a6..b4b96efede0 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp @@ -69,9 +69,9 @@ static irep_idt find_enum_function_on_stack(const call_stackt &context) /// otherwise. tvt java_enum_static_init_unwind_handler( const call_stackt &context, - unsigned loop_number, - unsigned unwind_count, - unsigned &unwind_max, + std::size_t loop_number, + std::size_t unwind_count, + std::size_t &unwind_max, const symbol_tablet &symbol_table) { (void)loop_number; // unused parameter diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h index 4fbb63c18ff..2f7694d3ae4 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h @@ -19,9 +19,9 @@ class symbol_tablet; tvt java_enum_static_init_unwind_handler( const call_stackt &context, - unsigned loop_number, - unsigned unwind_count, - unsigned &unwind_max, + std::size_t loop_number, + std::size_t unwind_count, + std::size_t &unwind_max, const symbol_tablet &symbol_table); #endif // CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index d3822c3abed..c64436d8c0b 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -203,19 +203,19 @@ static void gather_transitive_predecessors( /// slot `slotidx` static bool is_store_to_slot( const java_bytecode_convert_methodt::instructiont &inst, - unsigned slotidx) + std::size_t slotidx) { const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic; if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store")) return false; - unsigned storeslotidx; + std::size_t storeslotidx; if(inst.args.size()==1) { // Store with an argument: const auto &arg=inst.args[0]; - storeslotidx = numeric_cast_v(to_constant_expr(arg)); + storeslotidx = numeric_cast_v(to_constant_expr(arg)); } else { diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index a6d252f99e6..656ee871e16 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com void custom_bitvector_domaint::set_bit( const irep_idt &identifier, - unsigned bit_nr, + std::size_t bit_nr, modet mode) { switch(mode) @@ -48,7 +48,7 @@ void custom_bitvector_domaint::set_bit( void custom_bitvector_domaint::set_bit( const exprt &lhs, - unsigned bit_nr, + std::size_t bit_nr, modet mode) { irep_idt id=object2id(lhs); @@ -174,8 +174,7 @@ custom_bitvector_domaint::vectorst return vectorst(); } -unsigned custom_bitvector_analysist::get_bit_nr( - const exprt &string_expr) +std::size_t custom_bitvector_analysist::get_bit_nr(const exprt &string_expr) { if(string_expr.id()==ID_typecast) return get_bit_nr(to_typecast_expr(string_expr).op()); @@ -327,7 +326,8 @@ void custom_bitvector_domaint::transform( { if(instruction.call_arguments().size() == 2) { - unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]); + const std::size_t bit_nr = + cba.get_bit_nr(instruction.call_arguments()[1]); // initialize to make Visual Studio happy modet mode = modet::SET_MUST; @@ -456,7 +456,7 @@ void custom_bitvector_domaint::transform( DATA_INVARIANT( code.operands().size() == 2, "set/clear_may/must has two operands"); - unsigned bit_nr = cba.get_bit_nr(code.op1()); + const std::size_t bit_nr = cba.get_bit_nr(code.op1()); // initialize to make Visual Studio happy modet mode = modet::SET_MUST; @@ -578,7 +578,7 @@ void custom_bitvector_domaint::output( out << bit.first << " MAY:"; bit_vectort b=bit.second; - for(unsigned i=0; b!=0; i++, b>>=1) + for(std::size_t i = 0; b != 0; i++, b >>= 1) if(b&1) { INVARIANT(i < cba.bits.size(), "inconsistent bit widths"); @@ -594,7 +594,7 @@ void custom_bitvector_domaint::output( out << bit.first << " MUST:"; bit_vectort b=bit.second; - for(unsigned i=0; b!=0; i++, b>>=1) + for(std::size_t i = 0; b != 0; i++, b >>= 1) if(b&1) { INVARIANT(i < cba.bits.size(), "inconsistent bit widths"); @@ -706,7 +706,7 @@ exprt custom_bitvector_domaint::eval( { if(src.operands().size()==2) { - unsigned bit_nr = + const std::size_t bit_nr = custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1()); exprt pointer = to_binary_expr(src).op0(); @@ -773,7 +773,7 @@ void custom_bitvector_analysist::check( bool use_xml, std::ostream &out) { - unsigned pass=0, fail=0, unknown=0; + std::size_t pass = 0, fail = 0, unknown = 0; for(const auto &gf_entry : goto_model.goto_functions.function_map) { diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 786811365dd..f34847bd1bb 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -116,21 +116,21 @@ class custom_bitvector_domaint:public ai_domain_baset private: enum class modet { SET_MUST, CLEAR_MUST, SET_MAY, CLEAR_MAY }; - void set_bit(const exprt &, unsigned bit_nr, modet); - void set_bit(const irep_idt &, unsigned bit_nr, modet); + void set_bit(const exprt &, std::size_t bit_nr, modet); + void set_bit(const irep_idt &, std::size_t bit_nr, modet); - static inline void set_bit(bit_vectort &dest, unsigned bit_nr) + static inline void set_bit(bit_vectort &dest, std::size_t bit_nr) { dest|=(1ll< return operator[](loc).eval(src, *this); } - unsigned get_bit_nr(const exprt &); + std::size_t get_bit_nr(const exprt &); typedef numberingt bitst; bitst bits; diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h index 09bf46207f4..9fbb0842268 100644 --- a/src/analyses/invariant_propagation.h +++ b/src/analyses/invariant_propagation.h @@ -54,7 +54,7 @@ class invariant_propagationt:public inv_object_storet object_store; - typedef std::list object_listt; + typedef std::list object_listt; void add_objects(const goto_programt &goto_program); void add_objects(const goto_functionst &goto_functions); diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index f05476766e7..56ad434c0c4 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -29,7 +29,7 @@ void inv_object_storet::output(std::ostream &out) const out << "STORE " << i << ": " << map[i] << '\n'; } -bool inv_object_storet::get(const exprt &expr, unsigned &n) +bool inv_object_storet::get(const exprt &expr, std::size_t &n) { std::string s=build_string(expr); if(s.empty()) @@ -58,7 +58,7 @@ bool inv_object_storet::get(const exprt &expr, unsigned &n) return true; } -unsigned inv_object_storet::add(const exprt &expr) +std::size_t inv_object_storet::add(const exprt &expr) { std::string s=build_string(expr); CHECK_RETURN(!s.empty()); @@ -75,7 +75,7 @@ unsigned inv_object_storet::add(const exprt &expr) return n; } -bool inv_object_storet::is_constant(unsigned n) const +bool inv_object_storet::is_constant(std::size_t n) const { PRECONDITION(n < entries.size()); return entries[n].is_constant; @@ -147,9 +147,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const return ""; } -bool invariant_sett::get_object( - const exprt &expr, - unsigned &n) const +bool invariant_sett::get_object(const exprt &expr, std::size_t &n) const { return object_store.get(expr, n); } @@ -179,15 +177,15 @@ bool inv_object_storet::is_constant_address_rec(const exprt &expr) } void invariant_sett::add( - const std::pair &p, + const std::pair &p, ineq_sett &dest) { eq_set.check_index(p.first); eq_set.check_index(p.second); // add all. Quadratic. - unsigned f_r=eq_set.find(p.first); - unsigned s_r=eq_set.find(p.second); + std::size_t f_r = eq_set.find(p.first); + std::size_t s_r = eq_set.find(p.second); for(std::size_t f=0; f(f, s)); + dest.insert(std::pair(f, s)); } } } -void invariant_sett::add_eq(const std::pair &p) +void invariant_sett::add_eq(const std::pair &p) { eq_set.make_union(p.first, p.second); // check if there is a contradiction with two constants - unsigned r=eq_set.find(p.first); + std::size_t r = eq_set.find(p.first); bool constant_seen=false; mp_integer c; @@ -239,10 +237,10 @@ void invariant_sett::add_eq(const std::pair &p) void invariant_sett::add_eq( ineq_sett &dest, - const std::pair &eq, - const std::pair &ineq) + const std::pair &eq, + const std::pair &ineq) { - std::pair n; + std::pair n; // uhuh. Need to try all pairs @@ -275,9 +273,9 @@ void invariant_sett::add_eq( } } -tvt invariant_sett::is_eq(std::pair p) const +tvt invariant_sett::is_eq(std::pair p) const { - std::pair s=p; + std::pair s = p; std::swap(s.first, s.second); if(has_eq(p)) @@ -289,9 +287,9 @@ tvt invariant_sett::is_eq(std::pair p) const return tvt::unknown(); } -tvt invariant_sett::is_le(std::pair p) const +tvt invariant_sett::is_le(std::pair p) const { - std::pair s=p; + std::pair s = p; std::swap(s.first, s.second); if(has_eq(p)) @@ -363,7 +361,7 @@ void invariant_sett::add_type_bounds(const exprt &expr, const typet &type) // ">=" instead, and is meant to restrict types larger than a single byte? if(op_width<=8) { - unsigned a; + std::size_t a; if(get_object(expr, a)) return; @@ -434,7 +432,7 @@ void invariant_sett::strengthen_rec(const exprt &expr) return; } - std::pair p; + std::pair p; if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second)) return; @@ -531,7 +529,7 @@ void invariant_sett::strengthen_rec(const exprt &expr) add_type_bounds(equal_expr.op1(), typecast_expr.op().type()); } - std::pair p, s; + std::pair p, s; if( get_object(equal_expr.op0(), p.first) || @@ -560,7 +558,7 @@ void invariant_sett::strengthen_rec(const exprt &expr) { const auto ¬equal_expr = to_notequal_expr(expr); - std::pair p; + std::pair p; if( get_object(notequal_expr.op0(), p.first) || @@ -627,7 +625,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const { const auto &rel = to_binary_relation_expr(expr); - std::pair p; + std::pair p; bool ob0 = get_object(rel.lhs(), p.first); bool ob1 = get_object(rel.rhs(), p.second); @@ -672,7 +670,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const return tvt::unknown(); } -void invariant_sett::get_bounds(unsigned a, boundst &bounds) const +void invariant_sett::get_bounds(std::size_t a, boundst &bounds) const { // unbounded bounds=boundst(); @@ -830,7 +828,7 @@ void invariant_sett::simplify( exprt invariant_sett::get_constant(const exprt &expr) const { - unsigned a; + std::size_t a; if(!get_object(expr, a)) { @@ -843,7 +841,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const return from_integer(it->second.get_lower(), expr.type()); } - unsigned r=eq_set.find(a); + std::size_t r = eq_set.find(a); // is it a constant? for(std::size_t i=0; i(get_nil_irep()); } -std::string inv_object_storet::to_string(unsigned a) const +std::string inv_object_storet::to_string(std::size_t a) const { return id2string(map[a]); } -std::string invariant_sett::to_string(unsigned a) const +std::string invariant_sett::to_string(std::size_t a) const { return object_store.to_string(a); } @@ -915,7 +913,7 @@ bool invariant_sett::make_union(const invariant_sett &other) } // equalities first - unsigned old_eq_roots=eq_set.count_roots(); + std::size_t old_eq_roots = eq_set.count_roots(); eq_set.intersection(other.eq_set); @@ -970,7 +968,7 @@ bool invariant_sett::make_union_bounds_map(const bounds_mapt &other) return changed; } -void invariant_sett::modifies(unsigned a) +void invariant_sett::modifies(std::size_t a) { eq_set.isolate(a); remove(ne_set, a); @@ -983,7 +981,7 @@ void invariant_sett::modifies(const exprt &lhs) if(lhs.id()==ID_symbol || lhs.id()==ID_member) { - unsigned a; + std::size_t a; if(!get_object(lhs, a)) modifies(a); } diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index 72bcaf1984c..16a6465e772 100644 --- a/src/analyses/invariant_set.h +++ b/src/analyses/invariant_set.h @@ -33,21 +33,21 @@ class inv_object_storet { } - bool get(const exprt &expr, unsigned &n); + bool get(const exprt &expr, std::size_t &n); - unsigned add(const exprt &expr); + std::size_t add(const exprt &expr); - bool is_constant(unsigned n) const; + bool is_constant(std::size_t n) const; bool is_constant(const exprt &expr) const; static bool is_constant_address(const exprt &expr); - const irep_idt &operator[](unsigned n) const + const irep_idt &operator[](std::size_t n) const { return map[n]; } - const exprt &get_expr(unsigned n) const + const exprt &get_expr(std::size_t n) const { PRECONDITION(n < entries.size()); return entries[n].expr; @@ -55,7 +55,7 @@ class inv_object_storet void output(std::ostream &out) const; - std::string to_string(unsigned n) const; + std::string to_string(std::size_t n) const; protected: const namespacet &ns; @@ -83,7 +83,7 @@ class invariant_sett unsigned_union_find eq_set; // <= - typedef std::set > ineq_sett; + typedef std::set> ineq_sett; ineq_sett le_set; // != @@ -91,7 +91,7 @@ class invariant_sett // bounds typedef interval_templatet boundst; - typedef std::map bounds_mapt; + typedef std::map bounds_mapt; bounds_mapt bounds_map; bool threaded; @@ -164,7 +164,7 @@ class invariant_sett } } - static void remove(ineq_sett &dest, unsigned a) + static void remove(ineq_sett &dest, std::size_t a) { for(ineq_sett::iterator it=dest.begin(); it!=dest.end(); @@ -195,84 +195,82 @@ class invariant_sett void add_type_bounds(const exprt &expr, const typet &type); - void add_bounds(unsigned a, const boundst &bound) + void add_bounds(std::size_t a, const boundst &bound) { bounds_map[a].intersect_with(bound); } - void get_bounds(unsigned a, boundst &dest) const; + void get_bounds(std::size_t a, boundst &dest) const; // true = added something bool make_union_bounds_map(const bounds_mapt &other); - void modifies(unsigned a); + void modifies(std::size_t a); - std::string to_string(unsigned a) const; + std::string to_string(std::size_t a) const; - bool get_object( - const exprt &expr, - unsigned &n) const; + bool get_object(const exprt &expr, std::size_t &n) const; exprt get_constant(const exprt &expr) const; // queries - bool has_eq(const std::pair &p) const + bool has_eq(const std::pair &p) const { return eq_set.same_set(p.first, p.second); } - bool has_le(const std::pair &p) const + bool has_le(const std::pair &p) const { return le_set.find(p)!=le_set.end(); } - bool has_ne(const std::pair &p) const + bool has_ne(const std::pair &p) const { return ne_set.find(p)!=ne_set.end(); } - tvt is_eq(std::pair p) const; - tvt is_le(std::pair p) const; + tvt is_eq(std::pair p) const; + tvt is_le(std::pair p) const; - tvt is_lt(std::pair p) const + tvt is_lt(std::pair p) const { return is_le(p) && !is_eq(p); } - tvt is_ge(std::pair p) const + tvt is_ge(std::pair p) const { std::swap(p.first, p.second); return is_eq(p) || is_lt(p); } - tvt is_gt(std::pair p) const + tvt is_gt(std::pair p) const { return !is_le(p); } - tvt is_ne(std::pair p) const + tvt is_ne(std::pair p) const { return !is_eq(p); } - void add(const std::pair &p, ineq_sett &dest); + void add(const std::pair &p, ineq_sett &dest); - void add_le(const std::pair &p) + void add_le(const std::pair &p) { add(p, le_set); } - void add_ne(const std::pair &p) + void add_ne(const std::pair &p) { add(p, ne_set); } - void add_eq(const std::pair &eq); + void add_eq(const std::pair &eq); void add_eq( ineq_sett &dest, - const std::pair &eq, - const std::pair &ineq); + const std::pair &eq, + const std::pair &ineq); }; #endif // CPROVER_ANALYSES_INVARIANT_SET_H diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index d55b5d57293..837784bf265 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -51,7 +51,7 @@ void local_may_aliast::assign_lhs( { if(lhs.type().id()==ID_pointer) { - unsigned dest_pointer=objects.number(lhs); + const std::size_t dest_pointer = objects.number(lhs); // isolate the lhs pointer loc_info_dest.aliases.isolate(dest_pointer); @@ -154,7 +154,7 @@ bool local_may_aliast::aliases( tmp2.find(unknown_object)!=tmp2.end()) return true; - std::list result; + std::list result; std::set_intersection( tmp1.begin(), tmp1.end(), @@ -180,7 +180,7 @@ void local_may_aliast::get_rec( { if(rhs.type().id()==ID_pointer) { - unsigned src_pointer=objects.number(rhs); + const std::size_t src_pointer = objects.number(rhs); dest.insert(src_pointer); @@ -202,7 +202,7 @@ void local_may_aliast::get_rec( if(object.id()==ID_symbol) { - unsigned object_nr=objects.number(rhs); + const std::size_t object_nr = objects.number(rhs); dest.insert(object_nr); for(std::size_t i=0; i object_sett; + typedef std::set object_sett; void get_rec( object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const; - unsigned unknown_object; + std::size_t unknown_object; }; class local_may_alias_factoryt diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp index 50b156e2ca1..cdddc313097 100644 --- a/src/ansi-c/ansi_c_typecheck.cpp +++ b/src/ansi-c/ansi_c_typecheck.cpp @@ -39,7 +39,7 @@ bool ansi_c_typecheck( message_handlert &message_handler, const namespacet &ns) { - const unsigned errors_before= + const std::size_t errors_before = message_handler.get_message_count(messaget::M_ERROR); symbol_tablet symbol_table; diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp index f11ca833b0c..0836e086424 100644 --- a/src/ansi-c/literals/convert_integer_literal.cpp +++ b/src/ansi-c/literals/convert_integer_literal.cpp @@ -108,7 +108,7 @@ exprt convert_integer_literal(const std::string &src) ((signed?!is_unsigned:(is_unsigned || is_hex_or_oct_or_bin)) && \ (power(2, signed?width-1:width)>value_abs)) - unsigned width; + std::size_t width; bool is_signed=false; irep_idt c_type; diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp index dbb79e0d5ea..898093d8ba9 100644 --- a/src/cpp/cpp_token_buffer.cpp +++ b/src/cpp/cpp_token_buffer.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_token_buffer.h" -int cpp_token_buffert::LookAhead(unsigned offset) +int cpp_token_buffert::LookAhead(std::size_t offset) { PRECONDITION(current_pos <= token_vector.size()); @@ -51,7 +51,7 @@ int cpp_token_buffert::get_token() return kind; } -int cpp_token_buffert::LookAhead(unsigned offset, cpp_tokent &token) +int cpp_token_buffert::LookAhead(std::size_t offset, cpp_tokent &token) { PRECONDITION(current_pos <= token_vector.size()); diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h index 0721c85878d..309a35b2377 100644 --- a/src/cpp/cpp_token_buffer.h +++ b/src/cpp/cpp_token_buffer.h @@ -38,12 +38,12 @@ class cpp_token_buffert ansi_c_scanner_init(ansi_c_parser); } - typedef unsigned int post; + typedef std::size_t post; - int LookAhead(unsigned offset); + int LookAhead(std::size_t offset); int get_token(cpp_tokent &token); int get_token(); - int LookAhead(unsigned offset, cpp_tokent &token); + int LookAhead(std::size_t offset, cpp_tokent &token); post Save(); void Restore(post pos); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 4a8fb80c8e7..afa2f51d767 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -150,7 +150,7 @@ bool cpp_typecheck( message_handlert &message_handler, const namespacet &ns) { - const unsigned errors_before= + const std::size_t errors_before = message_handler.get_message_count(messaget::M_ERROR); symbol_tablet symbol_table; diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 777f4b2f0bd..25d867ec11a 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -269,7 +269,7 @@ class Parser // NOLINT(readability/identifiers) bool rSimpleDeclaration(cpp_declarationt &); bool isConstructorDecl(); - bool isPtrToMember(int); + bool isPtrToMember(std::size_t); bool optMemberSpec(cpp_member_spect &); bool optStorageSpec(cpp_storage_spect &); bool optCvQualify(typet &); @@ -1909,7 +1909,7 @@ bool Parser::isConstructorDecl() return false; // it's a declarator else if(t==TOK_STDCALL || t==TOK_FASTCALL || t==TOK_CLRCALL || t==TOK_CDECL) return false; // it's a declarator - else if(isPtrToMember(1)) + else if(isPtrToMember(1u)) return false; // declarator (::*) else if(is_identifier(t)) { @@ -1928,32 +1928,32 @@ bool Parser::isConstructorDecl() ptr.to.member : {'::'} (identifier {'<' any* '>'} '::')+ '*' */ -bool Parser::isPtrToMember(int i) +bool Parser::isPtrToMember(std::size_t i) { - int t0=lex.LookAhead(i++); + auto t0 = lex.LookAhead(i++); if(t0==TOK_SCOPE) t0=lex.LookAhead(i++); while(is_identifier(t0)) { - int t=lex.LookAhead(i++); + auto t = lex.LookAhead(i++); if(t=='<') { int n=1; while(n > 0) { - int u=lex.LookAhead(i++); + const auto u = lex.LookAhead(i++); if(u=='<') ++n; else if(u=='>') --n; else if(u=='(') { - int m=1; + std::size_t m = 1; while(m > 0) { - int v=lex.LookAhead(i++); + const auto v = lex.LookAhead(i++); if(v=='(') ++m; else if(v==')') @@ -3364,7 +3364,7 @@ bool Parser::optPtrOperator(typet &ptrs) t_list.push_back(op); } - else if(isPtrToMember(0)) + else if(isPtrToMember(0u)) { typet op; if(!rPtrToMember(op)) @@ -7132,8 +7132,8 @@ bool Parser::moreVarName() */ bool Parser::maybeTemplateArgs() { - int i=0; - int t=lex.LookAhead(i++); + std::size_t i = 0; + const auto t = lex.LookAhead(i++); #ifdef DEBUG indenter _i; @@ -7145,7 +7145,7 @@ bool Parser::maybeTemplateArgs() #if 1 for(;;) { - int u=lex.LookAhead(i++); + const auto u = lex.LookAhead(i++); if(u=='\0' || u==';' || u=='}') return false; else if((u=='>' || u==TOK_SHIFTRIGHT) && diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3631189d812..9fa1369dc40 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -93,7 +93,7 @@ bool compilet::doit() return true; } - const unsigned warnings_before = + const std::size_t warnings_before = log.get_message_handler().get_message_count(messaget::M_WARNING); auto symbol_table_opt = compile(); diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index 56bd0c198d6..bfb73964048 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -118,12 +118,12 @@ void symex_bmct::merge_goto( bool symex_bmct::should_stop_unwind( const symex_targett::sourcet &source, const call_stackt &context, - unsigned unwind) + std::size_t unwind) { const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc); tvt abort_unwind_decision; - unsigned this_loop_limit = std::numeric_limits::max(); + std::size_t this_loop_limit = std::numeric_limits::max(); for(auto handler : loop_unwind_handlers) { @@ -152,7 +152,7 @@ bool symex_bmct::should_stop_unwind( log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id << " iteration " << unwind; - if(this_loop_limit != std::numeric_limits::max()) + if(this_loop_limit != std::numeric_limits::max()) log.statistics() << " (" << this_loop_limit << " max)"; log.statistics() << " " << source.pc->source_location() << " thread " @@ -163,11 +163,11 @@ bool symex_bmct::should_stop_unwind( bool symex_bmct::get_unwind_recursion( const irep_idt &id, - unsigned thread_nr, - unsigned unwind) + std::size_t thread_nr, + std::size_t unwind) { tvt abort_unwind_decision; - unsigned this_loop_limit = std::numeric_limits::max(); + std::size_t this_loop_limit = std::numeric_limits::max(); for(auto handler : recursion_unwind_handlers) { @@ -199,7 +199,7 @@ bool symex_bmct::get_unwind_recursion( log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion " << symbol.display_name() << " iteration " << unwind; - if(this_loop_limit != std::numeric_limits::max()) + if(this_loop_limit != std::numeric_limits::max()) log.statistics() << " (" << this_loop_limit << " max)"; log.statistics() << log.eom; diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h index 8f484482cf4..8a59bca86c8 100644 --- a/src/goto-checker/symex_bmc.h +++ b/src/goto-checker/symex_bmc.h @@ -42,7 +42,7 @@ class symex_bmct : public goto_symext /// enforced. They return true to halt unwinding, false to authorise /// unwinding, or Unknown to indicate they have no opinion. typedef std::function< - tvt(const call_stackt &, unsigned, unsigned, unsigned &)> + tvt(const call_stackt &, std::size_t, std::size_t, std::size_t &)> loop_unwind_handlert; /// Recursion unwind handlers take the function ID, the unwind count so far, @@ -51,7 +51,7 @@ class symex_bmct : public goto_symext /// information for the user (e.g. "unwinding iteration N, max M"), /// and is not enforced. They return true to halt unwinding, false to /// authorise unwinding, or Unknown to indicate they have no opinion. - typedef std::function + typedef std::function recursion_unwind_handlert; /// Add a callback function that will be called to determine whether to unwind @@ -102,12 +102,12 @@ class symex_bmct : public goto_symext bool should_stop_unwind( const symex_targett::sourcet &source, const call_stackt &context, - unsigned unwind) override; + std::size_t unwind) override; bool get_unwind_recursion( const irep_idt &identifier, - unsigned thread_nr, - unsigned unwind) override; + std::size_t thread_nr, + std::size_t unwind) override; symex_coveraget symex_coverage; }; diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.h b/src/goto-checker/symex_bmc_incremental_one_loop.h index b5081081617..8a1b1d793bf 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.h +++ b/src/goto-checker/symex_bmc_incremental_one_loop.h @@ -35,20 +35,20 @@ class symex_bmc_incremental_one_loopt : public symex_bmct protected: const irep_idt incr_loop_id; - const unsigned incr_max_unwind; - const unsigned incr_min_unwind; + const std::size_t incr_max_unwind; + const std::size_t incr_min_unwind; std::unique_ptr state; // returns true if the symbolic execution is to be interrupted for checking - bool check_break(const irep_idt &loop_id, unsigned unwind) override; + bool check_break(const irep_idt &loop_id, std::size_t unwind) override; bool should_stop_unwind( const symex_targett::sourcet &source, const call_stackt &context, - unsigned unwind) override; + std::size_t unwind) override; - void log_unwinding(unsigned unwind); + void log_unwinding(std::size_t unwind); ui_message_handlert::uit output_ui; }; diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 9fbeaa5875b..1d54fb4c789 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -514,9 +514,9 @@ void acceleratet::build_state_machine( symbol_exprt next_state, scratch_programt &state_machine) { - std::map successor_counts; - unsigned int max_count=0; - unsigned int likely_next=0; + std::map successor_counts; + std::size_t max_count = 0; + std::size_t likely_next = 0; // Optimisation: find the most common successor state and initialise // next_state to that value. This reduces the size of the state machine @@ -524,8 +524,8 @@ void acceleratet::build_state_machine( for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p) { trace_automatont::state_pairt state_pair=p->second; - unsigned int to=state_pair.second; - unsigned int count=0; + const auto to = state_pair.second; + std::size_t count = 0; if(successor_counts.find(to)==successor_counts.end()) { @@ -569,8 +569,8 @@ void acceleratet::build_state_machine( for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p) { trace_automatont::state_pairt state_pair=p->second; - unsigned int from=state_pair.first; - unsigned int to=state_pair.second; + const auto from = state_pair.first; + const auto to = state_pair.second; if(to==likely_next) { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index a0a6dcd37ad..8786f762571 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -1207,7 +1207,7 @@ void acceleration_utilst::extract_polynomial( expr_listt terms=it->first; exprt coefficient=it->second; constant_exprt concrete_term=to_constant_expr(program.eval(coefficient)); - std::map degrees; + std::map degrees; mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true); monomial.coeff = numeric_cast_v(mp); @@ -1229,13 +1229,11 @@ void acceleration_utilst::extract_polynomial( } } - for(std::map::iterator it=degrees.begin(); - it!=degrees.end(); - ++it) + for(const auto °_pair : degrees) { monomialt::termt term; - term.var=it->first; - term.exp=it->second; + term.var = deg_pair.first; + term.exp = deg_pair.second; monomial.terms.push_back(term); } diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index 4cc36844cce..ffbd1247cde 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -40,7 +40,7 @@ bool all_paths_enumeratort::next(patht &path) std::cout << "Enumerating next path...\n"; #endif - int decision=backtrack(last_path); + std::size_t decision = backtrack(last_path); complete_path(last_path, decision); if(is_looping(last_path)) @@ -56,7 +56,7 @@ bool all_paths_enumeratort::next(patht &path) return false; } -int all_paths_enumeratort::backtrack(patht &path) +std::size_t all_paths_enumeratort::backtrack(patht &path) { // If we have a path of length 1 or 0, we can't backtrack any further. // That means we're done enumerating paths! @@ -72,7 +72,7 @@ int all_paths_enumeratort::backtrack(patht &path) goto_programt::targett parent_loc=path.back().loc; const auto succs=goto_program.get_successors(parent_loc); - unsigned int ret=0; + std::size_t ret = 0; for(const auto &succ : succs) { @@ -97,7 +97,7 @@ int all_paths_enumeratort::backtrack(patht &path) return backtrack(path); } -void all_paths_enumeratort::complete_path(patht &path, int succ) +void all_paths_enumeratort::complete_path(patht &path, std::size_t succ) { if(path.empty()) return; @@ -116,7 +116,7 @@ void all_paths_enumeratort::complete_path(patht &path, int succ) void all_paths_enumeratort::extend_path( patht &path, goto_programt::targett t, - int succ) + std::size_t succ) { goto_programt::targett next; exprt guard=true_exprt(); diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.h b/src/goto-instrument/accelerate/all_paths_enumerator.h index 3bd1b6b9ac6..96bf5ccc583 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.h +++ b/src/goto-instrument/accelerate/all_paths_enumerator.h @@ -35,9 +35,9 @@ class all_paths_enumeratort:public path_enumeratort virtual bool next(patht &path); protected: - int backtrack(patht &path); - void complete_path(patht &path, int succ); - void extend_path(patht &path, goto_programt::targett t, int succ); + std::size_t backtrack(patht &path); + void complete_path(patht &path, std::size_t succ); + void extend_path(patht &path, goto_programt::targett t, std::size_t succ); bool is_looping(patht &path); goto_programt &goto_program; diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp index e9f4f910b04..c63e98cc242 100644 --- a/src/goto-instrument/accelerate/polynomial.cpp +++ b/src/goto-instrument/accelerate/polynomial.cpp @@ -351,8 +351,8 @@ int monomialt::compare(monomialt &other) // are sorted according to string comparison on variable names. while(it!=terms.end() && jt != other.terms.end()) { - unsigned int e1=it->exp; - unsigned int e2=it->exp; + const auto e1 = it->exp; + const auto e2 = it->exp; int res=it->var.compare(jt->var); if(res < 0) @@ -405,10 +405,10 @@ int monomialt::compare(monomialt &other) UNREACHABLE; } -int polynomialt::max_degree(const exprt &var) +std::size_t polynomialt::max_degree(const exprt &var) { // We want the degree of the highest degree monomial in which `var' appears. - int maxd=0; + std::size_t maxd = 0; for(std::vector::iterator it=monomials.begin(); it!=monomials.end(); @@ -453,9 +453,9 @@ int polynomialt::coeff(const exprt &var) return 0; } -int monomialt::degree() +std::size_t monomialt::degree() { - int deg=0; + std::size_t deg = 0; for(std::vector::iterator it=terms.begin(); it!=terms.end(); diff --git a/src/goto-instrument/accelerate/polynomial.h b/src/goto-instrument/accelerate/polynomial.h index ac8ceb05034..b35f1d90028 100644 --- a/src/goto-instrument/accelerate/polynomial.h +++ b/src/goto-instrument/accelerate/polynomial.h @@ -23,7 +23,7 @@ class monomialt struct termt { exprt var; - unsigned int exp; // This means exponent, not expression. + std::size_t exp; // This means exponent, not expression. }; // Invariant: this vector is sorted lexicographically w.r.t. the variable. @@ -32,7 +32,7 @@ class monomialt int compare(monomialt &other); - int degree(); + std::size_t degree(); bool contains(const exprt &var); }; @@ -56,7 +56,7 @@ class polynomialt void mult(int scalar); void mult(polynomialt &other); - int max_degree(const exprt &var); + std::size_t max_degree(const exprt &var); int coeff(const exprt &expr); }; diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index ba6e4c3ce10..2166b2efd3b 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -354,7 +354,7 @@ void trace_automatont::get_transitions(sym_mapt &transitions) for(const auto &trans : dta_transitions) { goto_programt::targett l=trans.first; - unsigned int j=trans.second; + const auto j = trans.second; // We have a transition: i -l-> j. state_pairt state_pair(i, j); @@ -411,7 +411,7 @@ void automatont::reverse(goto_programt::targett epsilon) for(const auto &t : trans) { goto_programt::targett l=t.first; - unsigned int j=t.second; + const auto j = t.second; // There was a transition i -l-> j, so add a transition // j -l-> i. @@ -438,7 +438,7 @@ void automatont::trim() for(const auto &t : trans) { - unsigned int j=t.second; + const auto j = t.second; if(reachable.find(j)==reachable.end()) { diff --git a/src/goto-instrument/accelerate/trace_automaton.h b/src/goto-instrument/accelerate/trace_automaton.h index c3969df05b0..11b60d4f4b8 100644 --- a/src/goto-instrument/accelerate/trace_automaton.h +++ b/src/goto-instrument/accelerate/trace_automaton.h @@ -21,7 +21,7 @@ Author: Matt Lewis #include #include -typedef unsigned int statet; +typedef std::size_t statet; typedef std::set state_sett; class automatont diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index a6aaa4f114d..d2fe88294fa 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -353,7 +353,7 @@ void remove_repetition(std::set &exprs) { std::set signs1 = sign_of_expr(c, x); std::set signs2 = sign_of_expr(c, y); - int s1 = signs1.size(), s2 = signs2.size(); + std::size_t s1 = signs1.size(), s2 = signs2.size(); // it is easy to check non-equivalence; if(s1 != s2) { diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp index 9c6aa50aff4..d2fb4b60870 100644 --- a/src/goto-instrument/document_properties.cpp +++ b/src/goto-instrument/document_properties.cpp @@ -69,7 +69,7 @@ class document_propertiest void document_propertiest::strip_space(std::list &lines) { - unsigned strip=50; + std::size_t strip = 50; for(std::list::const_iterator it=lines.begin(); it!=lines.end(); it++) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 7381dfd302f..b696e71b837 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -939,9 +939,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( it->case_last->location_number > max_target->location_number) max_target=it->case_last; - std:: - map - targets_done; + std::map< + goto_programt::const_targett, + std::size_t, + goto_programt::target_less_than> + targets_done; loop_last_stack.push_back(std::make_pair(max_target, false)); // iterate over all diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 7dc097efd03..cd912af0ef2 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -33,14 +33,14 @@ void unwindsett::parse_unwindset_one_loop( if(val.empty()) return; - std::optional thread_nr; + std::optional thread_nr; if(isdigit(val[0])) { auto c_pos = val.find(':'); if(c_pos != std::string::npos) { std::string nr = val.substr(0, c_pos); - thread_nr = unsafe_string2unsigned(nr); + thread_nr = unsafe_string2size_t(nr); val.erase(0, nr.size() + 1); } } @@ -170,7 +170,7 @@ void unwindsett::parse_unwindset_one_loop( if(thread_nr.has_value()) { - thread_loop_map[std::pair(id, *thread_nr)] = uw; + thread_loop_map[std::pair(id, *thread_nr)] = uw; } else { @@ -188,13 +188,13 @@ void unwindsett::parse_unwindset( } std::optional -unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const +unwindsett::get_limit(const irep_idt &loop_id, std::size_t thread_nr) const { // We use the most specific limit we have // thread x loop auto tl_it = - thread_loop_map.find(std::pair(loop_id, thread_nr)); + thread_loop_map.find(std::pair(loop_id, thread_nr)); if(tl_it != thread_loop_map.end()) return tl_it->second; diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h index 4e3ffde0445..24431b33b20 100644 --- a/src/goto-instrument/unwindset.h +++ b/src/goto-instrument/unwindset.h @@ -44,7 +44,7 @@ class unwindsett // queries std::optional - get_limit(const irep_idt &loop, unsigned thread_id) const; + get_limit(const irep_idt &loop, std::size_t thread_id) const; // read unwindset directives from a file void parse_unwindset_file( @@ -63,7 +63,7 @@ class unwindsett // separate limits per thread using thread_loop_mapt = - std::map, std::optional>; + std::map, std::optional>; thread_loop_mapt thread_loop_map; void parse_unwindset_one_loop( diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-instrument/wmm/data_dp.cpp index 36588802ec4..848d9ae166c 100644 --- a/src/goto-instrument/wmm/data_dp.cpp +++ b/src/goto-instrument/wmm/data_dp.cpp @@ -123,7 +123,7 @@ void data_dpt::dp_merge() if(data.size()<2) return; - unsigned initial_size=data.size(); + std::size_t initial_size = data.size(); unsigned from=0; unsigned to=0; diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index fc33f29f75b..3951682e3a4 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -116,8 +116,8 @@ unsigned instrumentert::goto2graph_cfg( << visitor.max_thread << messaget::eom; /* SCCs which could host critical cycles */ - unsigned interesting_sccs=0; - for(unsigned i=0; i3) interesting_sccs++; diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index 38aafd4ceb2..c0bc2de0bf0 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -316,7 +316,7 @@ class instrumentert /* critical cycles per SCC */ std::vector > set_of_cycles_per_SCC; - unsigned num_sccs; + std::size_t num_sccs; /* map from function to begin and end of the corresponding part of the graph */ diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index bf4b85c69fe..9a247ef4d3c 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -170,9 +170,9 @@ void weak_memory( { instrumenter.collect_cycles_by_SCCs(model); message.status()<<"cycles collected: "<=4) { message.status()<<"SCC #"< #include @@ -25,13 +25,13 @@ class symbol_table_baset; bool write_goto_binary( std::ostream &out, const goto_modelt &, - int version=GOTO_BINARY_VERSION); + std::size_t version = GOTO_BINARY_VERSION); bool write_goto_binary( std::ostream &out, const symbol_table_baset &, const goto_functionst &, - int version = GOTO_BINARY_VERSION); + std::size_t version = GOTO_BINARY_VERSION); bool write_goto_binary( const std::string &filename, diff --git a/src/goto-symex/complexity_limiter.cpp b/src/goto-symex/complexity_limiter.cpp index 00e47c5b4f9..083553deda0 100644 --- a/src/goto-symex/complexity_limiter.cpp +++ b/src/goto-symex/complexity_limiter.cpp @@ -12,8 +12,6 @@ Author: John Dumbell #include "goto_symex_state.h" -#include - complexity_limitert::complexity_limitert( message_handlert &message_handler, const optionst &options) @@ -28,7 +26,7 @@ complexity_limitert::complexity_limitert( const std::size_t failed_child_loops_limit = options.get_signed_int_option( "symex-complexity-failed-child-loops-limit"); - const std::size_t unwind = options.get_signed_int_option("unwind"); + const int unwind = options.get_signed_int_option("unwind"); // If we have complexity enabled, try to work out a failed_children_limit. // In order of priority: @@ -38,7 +36,7 @@ complexity_limitert::complexity_limitert( if(failed_child_loops_limit > 0) max_loops_complexity = failed_child_loops_limit; else if(unwind > 0) - max_loops_complexity = std::max(static_cast(floor(unwind / 3)), 1); + max_loops_complexity = std::max(unwind / 3, 1); else max_loops_complexity = limit; } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index ae06ad54072..2bd3d8ff581 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -440,7 +440,7 @@ class goto_symext virtual bool should_stop_unwind( const symex_targett::sourcet &source, const call_stackt &context, - unsigned unwind); + std::size_t unwind); virtual void loop_bound_exceeded(statet &state, const exprt &guard); @@ -505,8 +505,8 @@ class goto_symext virtual bool get_unwind_recursion( const irep_idt &identifier, - unsigned thread_nr, - unsigned unwind); + std::size_t thread_nr, + std::size_t unwind); /// Iterates over \p arguments and assigns them to the parameters, which are /// symbols whose name and type are deduced from the type of \p goto_function. diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index fa7c06895f5..a8921e67b42 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -176,7 +176,7 @@ class goto_symex_statet final : public goto_statet void print_backtrace(std::ostream &) const; // threads - typedef std::pair > a_s_r_entryt; + typedef std::pair> a_s_r_entryt; typedef std::list a_s_w_entryt; std::unordered_map read_in_atomic_section; std::unordered_map diff --git a/src/goto-symex/memory_model.h b/src/goto-symex/memory_model.h index eb4cad75753..8f1f4e00d73 100644 --- a/src/goto-symex/memory_model.h +++ b/src/goto-symex/memory_model.h @@ -57,7 +57,7 @@ class memory_model_baset : public partial_order_concurrencyt symex_target_equationt &equation); // maps thread numbers to an event list - typedef std::map per_thread_mapt; + typedef std::map per_thread_mapt; }; #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_H diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index 9ff92da9824..277b028ef83 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -78,7 +78,7 @@ void partial_order_concurrencyt::build_event_lists( add_init_writes(equation); // a per-thread counter - std::map counter; + std::map counter; for(eventst::const_iterator e_it=equation.SSA_steps.begin(); @@ -89,7 +89,7 @@ void partial_order_concurrencyt::build_event_lists( e_it->is_shared_write() || e_it->is_spawn()) { - unsigned thread_nr=e_it->source.thread_nr; + std::size_t thread_nr = e_it->source.thread_nr; if(!e_it->is_spawn()) { diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 7109f4b0c09..ab9b5930b8d 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -128,7 +128,7 @@ void symex_level1t::restore_from(const symex_level1t &other) } } -unsigned symex_level2t::latest_index(const irep_idt &identifier) const +std::size_t symex_level2t::latest_index(const irep_idt &identifier) const { const auto r_opt = current_names.find(identifier); return !r_opt ? 0 : r_opt->get().second; diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index eda7865f59a..3e0301353aa 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -74,7 +74,7 @@ struct symex_level2t renamedt operator()(renamedt l1_expr) const; /// Counter corresponding to an identifier - unsigned latest_index(const irep_idt &identifier) const; + std::size_t latest_index(const irep_idt &identifier) const; /// Allocates a fresh L2 name for the given L1 identifier, and makes it the /// latest generation on this path. diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 6fdf9f4ff5e..ed20886c7ff 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -24,7 +24,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_storage.h" #include "symex_assign.h" -bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned) +bool goto_symext::get_unwind_recursion( + const irep_idt &, + std::size_t, + std::size_t) { return false; } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 8dcd92c6078..fe3756f39e8 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -742,8 +742,8 @@ static void merge_names( symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, - const unsigned goto_count, - const unsigned dest_count) + const std::size_t goto_count, + const std::size_t dest_count) { const irep_idt l1_identifier = ssa.get_identifier(); const irep_idt &obj_identifier = ssa.get_object_name(); @@ -876,10 +876,10 @@ void goto_symext::phi_function( for(const auto &delta_item : delta_view) { const ssa_exprt &ssa = delta_item.m.first; - unsigned goto_count = delta_item.m.second; - unsigned dest_count = !delta_item.is_in_both_maps() - ? 0 - : delta_item.get_other_map_value().second; + std::size_t goto_count = delta_item.m.second; + std::size_t dest_count = !delta_item.is_in_both_maps() + ? 0 + : delta_item.get_other_map_value().second; merge_names( goto_state, @@ -905,8 +905,8 @@ void goto_symext::phi_function( continue; const ssa_exprt &ssa = delta_item.m.first; - unsigned goto_count = 0; - unsigned dest_count = delta_item.m.second; + std::size_t goto_count = 0; + std::size_t dest_count = delta_item.m.second; merge_names( goto_state, @@ -954,7 +954,7 @@ void goto_symext::loop_bound_exceeded( bool goto_symext::should_stop_unwind( const symex_targett::sourcet &, const call_stackt &, - unsigned) + std::size_t) { // by default, we keep going return false; diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index de1e7f1f388..e9a2bd43d6d 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -276,7 +276,7 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state) } static void -switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb) +switch_to_thread(goto_symex_statet &state, const std::size_t thread_nb) { PRECONDITION(state.source.thread_nr < state.threads.size()); PRECONDITION(thread_nb < state.threads.size()); @@ -311,7 +311,7 @@ void goto_symext::symex_threaded_step( if(state.call_stack().empty() && state.source.thread_nr+1 function_numbering; - void set_from(const irep_idt &function, unsigned inx) + void set_from(const irep_idt &function, std::size_t inx) { from_function = function_numbering.number(function); from_target_index = inx; } - void set_to(const irep_idt &function, unsigned inx) + void set_to(const irep_idt &function, std::size_t inx) { to_function = function_numbering.number(function); to_target_index = inx; @@ -189,7 +189,7 @@ class value_set_fit typedef std::unordered_set expr_sett; - typedef std::unordered_set dynamic_object_id_sett; + typedef std::unordered_set dynamic_object_id_sett; typedef std::map valuest; typedef std::set flatten_seent; diff --git a/src/solvers/bdd/miniBDD/miniBDD.cpp b/src/solvers/bdd/miniBDD/miniBDD.cpp index ec7b87b5483..acc32e83755 100644 --- a/src/solvers/bdd/miniBDD/miniBDD.cpp +++ b/src/solvers/bdd/miniBDD/miniBDD.cpp @@ -56,7 +56,7 @@ void mini_bdd_mgrt::DumpDot(std::ostream &out, bool suppress_zero) const out << " { node [shape=box,fontsize=24]; \"1\"; }\n" << "}\n\n"; - for(unsigned v = 0; v < var_table.size(); v++) + for(std::size_t v = 0; v < var_table.size(); v++) { out << "{ rank=same; " "{ node [shape=plaintext,fontname=\"Times Italic\",fontsize=24] \" " @@ -75,7 +75,7 @@ void mini_bdd_mgrt::DumpDot(std::ostream &out, bool suppress_zero) const out << "{ edge [style = invis];"; - for(unsigned v = 0; v < var_table.size(); v++) + for(std::size_t v = 0; v < var_table.size(); v++) out << " \" " << var_table[v].label << " \" ->"; out << " \"T\"; }\n"; @@ -114,7 +114,7 @@ void mini_bdd_mgrt::DumpTikZ( out << " \\tikzstyle{BDDnode}=[circle,draw=black," "inner sep=0pt,minimum size=5mm]\n"; - for(unsigned v = 0; v < var_table.size(); v++) + for(std::size_t v = 0; v < var_table.size(); v++) { out << " \\node["; @@ -124,7 +124,7 @@ void mini_bdd_mgrt::DumpTikZ( out << "] (v" << var_table[v].label << ") {$\\mathit{" << var_table[v].label << "}$};\n"; - unsigned previous = 0; + std::size_t previous = 0; for(const auto &u : nodes) { @@ -198,7 +198,7 @@ class mini_bdd_applyt mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y); mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y); - typedef std::map, mini_bddt> Gt; + typedef std::map, mini_bddt> Gt; Gt G; }; @@ -212,7 +212,7 @@ mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y) "apply can only be called on BDDs with the same manager"); // dynamic programming - std::pair key(x.node_number(), y.node_number()); + std::pair key(x.node_number(), y.node_number()); Gt::const_iterator G_it = G.find(key); if(G_it != G.end()) return G_it->second; @@ -250,8 +250,8 @@ mini_bddt mini_bdd_applyt::APP_non_rec(const mini_bddt &_x, const mini_bddt &_y) { } mini_bddt &result, x, y, lr, hr; - std::pair key; - unsigned var; + std::pair key; + std::size_t var; enum class phaset { INIT, @@ -422,7 +422,7 @@ mini_bdd_mgrt::~mini_bdd_mgrt() } mini_bddt -mini_bdd_mgrt::mk(unsigned var, const mini_bddt &low, const mini_bddt &high) +mini_bdd_mgrt::mk(std::size_t var, const mini_bddt &low, const mini_bddt &high) { PRECONDITION_WITH_DIAGNOSTICS( var <= var_table.size(), "cannot make a BDD for an unknown variable"); @@ -447,7 +447,7 @@ mini_bdd_mgrt::mk(unsigned var, const mini_bddt &low, const mini_bddt &high) if(free.empty()) { - unsigned new_number = nodes.back().node_number + 1; + const std::size_t new_number = nodes.back().node_number + 1; nodes.push_back(mini_bdd_nodet(this, var, new_number, low, high)); n = &nodes.back(); } @@ -510,7 +510,7 @@ void mini_bdd_mgrt::DumpTable(std::ostream &out) const class restrictt { public: - inline restrictt(const unsigned _var, const bool _value) + inline restrictt(const std::size_t _var, const bool _value) : var(_var), value(_value) { } @@ -521,7 +521,7 @@ class restrictt } protected: - const unsigned var; + const std::size_t var; const bool value; mini_bddt RES(const mini_bddt &u); @@ -548,18 +548,18 @@ mini_bddt restrictt::RES(const mini_bddt &u) return t; } -mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value) +mini_bddt restrict(const mini_bddt &u, std::size_t var, const bool value) { return restrictt(var, value)(u); } -mini_bddt exists(const mini_bddt &u, const unsigned var) +mini_bddt exists(const mini_bddt &u, const std::size_t var) { // u[var/0] OR u[var/1] return restrict(u, var, false) | restrict(u, var, true); } -mini_bddt substitute(const mini_bddt &t, unsigned var, const mini_bddt &tp) +mini_bddt substitute(const mini_bddt &t, std::size_t var, const mini_bddt &tp) { // t[var/tp] = // ( tp &t[var/1]) | @@ -607,7 +607,7 @@ std::string cubes(const mini_bddt &u) } } -bool OneSat(const mini_bddt &v, std::map &assignment) +bool OneSat(const mini_bddt &v, std::map &assignment) { // http://www.ecs.umass.edu/ece/labs/vlsicad/ece667/reading/somenzi99bdd.pdf if(v.is_true()) diff --git a/src/solvers/bdd/miniBDD/miniBDD.h b/src/solvers/bdd/miniBDD/miniBDD.h index 4a1f8de179b..e95516c8318 100644 --- a/src/solvers/bdd/miniBDD/miniBDD.h +++ b/src/solvers/bdd/miniBDD/miniBDD.h @@ -48,10 +48,10 @@ class mini_bddt bool is_true() const; bool is_false() const; - unsigned var() const; + std::size_t var() const; const mini_bddt &low() const; const mini_bddt &high() const; - unsigned node_number() const; + std::size_t node_number() const; void clear(); bool is_initialized() const @@ -68,13 +68,13 @@ class mini_bdd_nodet { public: class mini_bdd_mgrt *mgr; - unsigned var, node_number, reference_counter; + std::size_t var, node_number, reference_counter; mini_bddt low, high; mini_bdd_nodet( class mini_bdd_mgrt *_mgr, - unsigned _var, - unsigned _node_number, + std::size_t _var, + std::size_t _node_number, const mini_bddt &_low, const mini_bddt &_high); @@ -103,7 +103,7 @@ class mini_bdd_mgrt friend class mini_bdd_nodet; // create a node (consulting the reverse-map) - mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high); + mini_bddt mk(std::size_t var, const mini_bddt &low, const mini_bddt &high); std::size_t number_of_nodes(); @@ -124,8 +124,11 @@ class mini_bdd_mgrt // this is our reverse-map for nodes struct reverse_keyt { - unsigned var, low, high; - reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high); + std::size_t var, low, high; + reverse_keyt( + std::size_t _var, + const mini_bddt &_low, + const mini_bddt &_high); bool operator<(const reverse_keyt &) const; }; @@ -137,12 +140,12 @@ class mini_bdd_mgrt freet free; }; -mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value); -mini_bddt exists(const mini_bddt &u, unsigned var); +mini_bddt restrict(const mini_bddt &u, std::size_t var, const bool value); +mini_bddt exists(const mini_bddt &u, std::size_t var); mini_bddt -substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what); +substitute(const mini_bddt &where, std::size_t var, const mini_bddt &by_what); std::string cubes(const mini_bddt &u); -bool OneSat(const mini_bddt &v, std::map &assignment); +bool OneSat(const mini_bddt &v, std::map &assignment); // inline functions #include "miniBDD.inc" // IWYU pragma: keep diff --git a/src/solvers/bdd/miniBDD/miniBDD.inc b/src/solvers/bdd/miniBDD/miniBDD.inc index a9de1cba622..a977dbaeeb5 100644 --- a/src/solvers/bdd/miniBDD/miniBDD.inc +++ b/src/solvers/bdd/miniBDD/miniBDD.inc @@ -51,13 +51,13 @@ inline bool mini_bddt::is_false() const return node->node_number==0; } -inline unsigned mini_bddt::var() const +inline std::size_t mini_bddt::var() const { PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized"); return node->var; } -inline unsigned mini_bddt::node_number() const +inline std::size_t mini_bddt::node_number() const { PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized"); return node->node_number; @@ -88,11 +88,16 @@ inline void mini_bddt::clear() inline mini_bdd_nodet::mini_bdd_nodet( class mini_bdd_mgrt *_mgr, - unsigned _var, unsigned _node_number, - const mini_bddt &_low, const mini_bddt &_high): - mgr(_mgr), var(_var), node_number(_node_number), - reference_counter(0), - low(_low), high(_high) + std::size_t _var, + std::size_t _node_number, + const mini_bddt &_low, + const mini_bddt &_high) + : mgr(_mgr), + var(_var), + node_number(_node_number), + reference_counter(0), + low(_low), + high(_high) { } @@ -117,8 +122,10 @@ inline void mini_bdd_nodet::add_reference() } inline mini_bdd_mgrt::reverse_keyt::reverse_keyt( - unsigned _var, const mini_bddt &_low, const mini_bddt &_high): - var(_var), low(_low.node->node_number), high(_high.node->node_number) + std::size_t _var, + const mini_bddt &_low, + const mini_bddt &_high) + : var(_var), low(_low.node->node_number), high(_high.node->node_number) { } diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp index 5add319eef2..8dd7ab9187e 100644 --- a/src/solvers/flattening/equality.cpp +++ b/src/solvers/flattening/equality.cpp @@ -45,11 +45,11 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2) elements_revt &elements_rev=typestruct.elements_rev; equalitiest &equalities=typestruct.equalities; - std::pair u; + std::pair u; { - std::pair result= - elements.insert(std::pair(e1, elements.size())); + std::pair result = + elements.insert({e1, elements.size()}); u.first=result.first->second; diff --git a/src/solvers/flattening/equality.h b/src/solvers/flattening/equality.h index d8f41158111..a70b26d869a 100644 --- a/src/solvers/flattening/equality.h +++ b/src/solvers/flattening/equality.h @@ -36,9 +36,9 @@ class equalityt:public prop_conv_solvert } protected: - typedef std::unordered_map elementst; - typedef std::map, literalt> equalitiest; - typedef std::map elements_revt; + typedef std::unordered_map elementst; + typedef std::map, literalt> equalitiest; + typedef std::map elements_revt; struct typestructt { diff --git a/src/solvers/floatbv/float_approximation.cpp b/src/solvers/floatbv/float_approximation.cpp index dd2bf6b5087..80804453df9 100644 --- a/src/solvers/floatbv/float_approximation.cpp +++ b/src/solvers/floatbv/float_approximation.cpp @@ -20,12 +20,12 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent) bvt new_exponent=prop.new_variables(exponent.size()); // i is the shift distance - for(unsigned i=0; i 0); exponent = typecast_exprt( exponent, signedbv_typet(std::max(depth, exponent_bits + 1))); exprt exponent_delta=from_integer(0, exponent.type()); - for(int d=depth-1; d>=0; d--) + for(std::size_t d = depth; d > 0; --d) { - unsigned distance=(1< distance, "distance must be within the range of fraction bits"); @@ -982,13 +983,9 @@ void float_bvt::normalization_shift( if_exprt(prefix_is_zero, shifted, fraction); // add corresponding weight to exponent - INVARIANT( - d < (signed int)exponent_bits, - "depth must be smaller than exponent bits"); - - exponent_delta= - bitor_exprt(exponent_delta, - shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d)); + exponent_delta = bitor_exprt( + exponent_delta, + shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d - 1)); } exponent=minus_exprt(exponent, exponent_delta); diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp index 9e8389e627a..97a31b6e5ab 100644 --- a/src/solvers/floatbv/float_utils.cpp +++ b/src/solvers/floatbv/float_utils.cpp @@ -806,9 +806,9 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent) bvt exponent_delta=bv_utils.zeros(exponent.size()); - for(int d=depth-1; d>=0; d--) + for(std::size_t d = depth; d > 0; --d) { - std::size_t distance=(1< distance, "fraction must be larger than distance"); @@ -825,10 +825,7 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent) bv_utils.select(prefix_is_zero, shifted, fraction); // add corresponding weight to exponent - INVARIANT( - d < (signed)exponent_delta.size(), - "depth must be smaller than exponent size"); - exponent_delta[d]=prefix_is_zero; + exponent_delta[d - 1] = prefix_is_zero; } exponent=bv_utils.sub(exponent, exponent_delta); diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index 4a002bcd2d5..b5a115564e6 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -60,7 +60,7 @@ class cover_goalst return _number_covered; } - unsigned iterations() const + std::size_t iterations() const { return _iterations; } @@ -94,7 +94,7 @@ class cover_goalst protected: std::size_t _number_covered; - unsigned _iterations; + std::size_t _iterations; decision_proceduret &decision_procedure; typedef std::vector observerst; diff --git a/src/solvers/qbf/qbf_qube_core.h b/src/solvers/qbf/qbf_qube_core.h index 8dfe7c8c1cb..62c3a504620 100644 --- a/src/solvers/qbf/qbf_qube_core.h +++ b/src/solvers/qbf/qbf_qube_core.h @@ -19,7 +19,7 @@ class qbf_qube_coret:public qdimacs_coret protected: std::string qbf_tmp_file; - typedef std::map assignmentt; + typedef std::map assignmentt; assignmentt assignment; public: diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index f55b56097be..afb543f0a39 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -29,13 +29,9 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) log.debug() << "Solving with " << prop.solver_text() << messaget::eom; - unsigned iteration=0; - // now enter the loop - while(true) + for(std::size_t iteration = 1; true; ++iteration) { - iteration++; - log.progress() << "BV-Refinement: iteration " << iteration << messaget::eom; // output the very same information in a structured fashion diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 64a1a63302f..9f88f22af0e 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -38,7 +38,7 @@ void bv_refinementt::arrays_overapproximated() if(!config_.refine_arrays) return; - unsigned nb_active=0; + std::size_t nb_active = 0; std::list::iterator it=lazy_array_constraints.begin(); while(it!=lazy_array_constraints.end()) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index c952506111f..41fc102dff8 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2_parser.h" -#include "smt2_format.h" - #include #include #include @@ -19,6 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include + +#include "smt2_format.h" #include @@ -507,7 +508,7 @@ exprt smt2_parsert::function_application() if(next_token() != smt2_tokenizert::NUMERAL) throw error("expected numeral as bitvector literal width"); - auto width = std::stoll(smt2_tokenizer.get_buffer()); + const auto width = safe_string2size_t(smt2_tokenizer.get_buffer()); if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' after bitvector literal"); @@ -623,12 +624,12 @@ exprt smt2_parsert::function_application() if(next_token() != smt2_tokenizert::NUMERAL) throw error("expected numeral after extract"); - auto upper = std::stoll(smt2_tokenizer.get_buffer()); + const auto upper = safe_string2size_t(smt2_tokenizer.get_buffer()); if(next_token() != smt2_tokenizert::NUMERAL) throw error("expected two numerals after extract"); - auto lower = std::stoll(smt2_tokenizer.get_buffer()); + const auto lower = safe_string2size_t(smt2_tokenizer.get_buffer()); if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' after extract"); diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index f439e5f28b3..a59fb142e04 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -372,13 +372,13 @@ exprt is_digit_with_radix( const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, - const unsigned long radix_ul); + const std::size_t radix_ul); exprt get_numeric_value_from_character( const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, - unsigned long radix_ul); + std::size_t radix_ul); #endif diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index 039557734a1..54b91048309 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -20,17 +20,15 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// If the expression is a constant expression then we get the value of it as -/// an unsigned long. If not we return a default value. +/// a std::size_t. If not we return a default value. /// \param expr: input expression /// \param def: default value to return if we cannot evaluate expr /// \param ns: namespace used to simplify the expression -/// \return the output as an unsigned long -static unsigned long to_integer_or_default( - const exprt &expr, - unsigned long def, - const namespacet &ns) +/// \return the output as a std::size_t +static std::size_t +to_integer_or_default(const exprt &expr, std::size_t def, const namespacet &ns) { - if(const auto i = numeric_cast(simplify_expr(expr, ns))) + if(const auto i = numeric_cast(simplify_expr(expr, ns))) return *i; return def; } @@ -146,7 +144,7 @@ string_constraint_generatort::add_axioms_for_string_of_int_with_radix( /// Most of the time we can evaluate radix as an integer. The value 0 is used /// to indicate when we can't tell what the radix is. - const unsigned long radix_ul = to_integer_or_default(radix, 0, ns); + const auto radix_ul = to_integer_or_default(radix, 0, ns); CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); if(max_size == 0) @@ -279,7 +277,7 @@ std::vector string_constraint_generatort::get_conjuncts_for_correct_number_format( const array_string_exprt &str, const exprt &radix_as_char, - const unsigned long radix_ul, + const std::size_t radix_ul, const std::size_t max_size, const bool strict_formatting) { @@ -367,7 +365,7 @@ string_constraint_generatort::get_conjuncts_for_correct_number_format( /// \param str: input string /// \param max_string_length: the maximum length str can have /// \param radix: the radix, with the same type as input_int -/// \param radix_ul: the radix as an unsigned long, or 0 if that can't be +/// \param radix_ul: the radix as a size_t, or 0 if that can't be /// determined string_constraintst string_constraint_generatort::add_axioms_for_characters_in_integer_string( @@ -377,7 +375,7 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string( const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, - const unsigned long radix_ul) + const std::size_t radix_ul) { string_constraintst constraints; const typet &char_type = to_type_with_subtype(str.content().type()).subtype(); @@ -469,7 +467,7 @@ string_constraint_generatort::unpack_parseint_arguments( : static_cast(typecast_exprt(f.arguments()[1], target_int_type)); // Most of the time we can evaluate radix as an integer. The value 0 is used // to indicate when we can't tell what the radix is. - const unsigned long radix_ul = to_integer_or_default(radix, 0, ns); + const auto radix_ul = to_integer_or_default(radix, 0, ns); PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); const std::size_t max_string_length = @@ -556,7 +554,7 @@ exprt is_digit_with_radix( const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, - const unsigned long radix_ul) + const std::size_t radix_ul) { PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0); const typet &char_type = chr.type(); @@ -625,7 +623,7 @@ exprt get_numeric_value_from_character( const typet &char_type, const typet &type, const bool strict_formatting, - const unsigned long radix_ul) + const std::size_t radix_ul) { const constant_exprt zero_char = from_integer('0', char_type); @@ -694,7 +692,7 @@ exprt get_numeric_value_from_character( /// \param radix_ul: the radix we are using, or 0, in which case the return /// value will work for any radix /// \return the maximum string length -size_t max_printed_string_length(const typet &type, unsigned long radix_ul) +size_t max_printed_string_length(const typet &type, std::size_t radix_ul) { if(radix_ul == 0) { diff --git a/src/util/graph.h b/src/util/graph.h index 9b9f6b6a5e8..b1cb95a197b 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -12,9 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_GRAPH_H #define CPROVER_UTIL_GRAPH_H +#include "invariant.h" + #include #include #include +#include #include #include #include @@ -22,8 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "invariant.h" - class empty_edget { }; @@ -332,8 +333,8 @@ class grapht { public: std::vector visited; - std::vector depth; - std::vector lowlink; + std::vector depth; + std::vector lowlink; std::vector in_scc; std::stack scc_stack; std::vector &subgraph_nr; @@ -423,12 +424,12 @@ void grapht::shortest_path( bool non_trivial) const { std::vector visited; - std::vector distance; - std::vector previous; + std::vector distance; + std::vector previous; // initialization visited.resize(nodes.size(), false); - distance.resize(nodes.size(), (unsigned)(-1)); + distance.resize(nodes.size(), std::numeric_limits::max()); previous.resize(nodes.size(), 0); if(!non_trivial) @@ -445,7 +446,7 @@ void grapht::shortest_path( frontier_set.push_back(src); - unsigned d=0; + std::size_t d = 0; bool found=false; while(!frontier_set.empty() && !found) @@ -493,7 +494,7 @@ void grapht::shortest_path( path.clear(); // reachable at all? - if(distance[dest]==(unsigned)(-1)) + if(distance[dest] == std::numeric_limits::max()) return; // nah while(true) diff --git a/src/util/string_expr.h b/src/util/string_expr.h index 0588b2dccdd..64b517aae43 100644 --- a/src/util/string_expr.h +++ b/src/util/string_expr.h @@ -87,7 +87,7 @@ class array_string_exprt : public exprt return index_exprt(content(), i); } - index_exprt operator[](int i) const + index_exprt operator[](std::size_t i) const { return index_exprt(content(), from_integer(i, length_type())); } diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp index 8a65e40fb3f..b08ee13d6c8 100644 --- a/src/util/typecheck.cpp +++ b/src/util/typecheck.cpp @@ -15,7 +15,7 @@ bool typecheckt::typecheck_main() { PRECONDITION(message_handler); - const unsigned errors_before= + const std::size_t errors_before = message_handler->get_message_count(messaget::M_ERROR); try diff --git a/src/xmllang/scanner.l b/src/xmllang/scanner.l index b4242d1a534..9b03b39b356 100755 --- a/src/xmllang/scanner.l +++ b/src/xmllang/scanner.l @@ -29,7 +29,7 @@ static char *word(char *s) { char *buf; - int i, k; + std::size_t i, k; for (k = 0; isspace(s[k]) || s[k] == '<'; k++) ; for (i = k; s[i] && ! isspace(s[i]); i++) ; buf = (char *)malloc((i - k + 1) * sizeof(char)); diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index d72b32ae765..b3cace9b394 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -80,7 +80,7 @@ SCENARIO("call_graph", THEN("We expect A -> { A, B, B }, B -> { C, D }") { const auto &check_graph=call_graph_from_goto_functions.edges; - REQUIRE(check_graph.size()==5); + REQUIRE(check_graph.size() == 5ULL); REQUIRE(multimap_key_matches(check_graph, "A", {"A", "B", "B"})); REQUIRE(multimap_key_matches(check_graph, "B", {"C", "D"})); } @@ -97,7 +97,7 @@ SCENARIO("call_graph", THEN("We expect A -> { A }, B -> { A, A }, C -> { B }, D -> { B }") { const auto &check_graph=inverse_call_graph_from_goto_functions.edges; - REQUIRE(check_graph.size()==5); + REQUIRE(check_graph.size() == 5ULL); REQUIRE(multimap_key_matches(check_graph, "A", {"A"})); REQUIRE(multimap_key_matches(check_graph, "B", {"A", "A"})); REQUIRE(multimap_key_matches(check_graph, "C", {"B"})); diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index 71a311e31a9..f622054de2f 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -58,7 +58,7 @@ class bdd_propt : public propt return const_literal(bdd.is_true()); std::size_t index = bdd.node_number(); bdd_map[index] = bdd; - return literalt(index, false); + return literalt(static_cast(index), false); } literalt land(literalt a, literalt b) override diff --git a/unit/util/format_number_range.cpp b/unit/util/format_number_range.cpp index 846362d2ab3..c912788ec02 100644 --- a/unit/util/format_number_range.cpp +++ b/unit/util/format_number_range.cpp @@ -12,7 +12,7 @@ Author: Michael Tautschnig #include TEST_CASE( - "Format a range of unsigned numbers", + "Format a range of std::size_t numbers", "[core][util][format_number_range]") { const std::vector singleton = {1}; diff --git a/unit/util/small_map.cpp b/unit/util/small_map.cpp index aa7e900f4ea..9d0cde98126 100644 --- a/unit/util/small_map.cpp +++ b/unit/util/small_map.cpp @@ -64,8 +64,8 @@ void small_map_test() int cnt = 0; for(auto it = m.begin(); it != m.end(); it++) { - REQUIRE(it->first == it->second); - REQUIRE((*it).first == (*it).second); + REQUIRE(static_cast(it->first) == it->second); + REQUIRE(static_cast((*it).first) == (*it).second); cnt++; } @@ -143,7 +143,7 @@ void small_map_test() for(std::size_t i = 0; i < small_mapt::NUM; i++) { - m[i] = i; + m[i] = static_cast(i); } for(std::size_t i = 0; i < small_mapt::NUM; i++) From 517390e7700189f7f692f4b08e90757102785926 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Dec 2018 18:23:14 +0000 Subject: [PATCH 12/18] Extend the usage of method_offsett --- .../java_bytecode_convert_method.cpp | 20 ++++---- .../java_bytecode_convert_method_class.h | 11 ++-- .../java_bytecode/java_bytecode_parse_tree.h | 16 +++--- .../java_bytecode/java_bytecode_parser.cpp | 4 +- .../java_local_variable_table.cpp | 50 +++++++++++-------- jbmc/src/java_bytecode/java_utils.cpp | 7 +-- jbmc/src/java_bytecode/java_utils.h | 2 +- 7 files changed, 60 insertions(+), 50 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 109e00ed632..4008cdc9bf0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -196,7 +196,7 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable( exprt java_bytecode_convert_methodt::variable( const exprt &arg, char type_char, - size_t address) + method_offsett address) { const std::size_t number_int = numeric_cast_v(to_constant_expr(arg)); @@ -942,7 +942,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( } static void gather_symbol_live_ranges( - java_bytecode_convert_methodt::method_offsett pc, + method_offsett pc, const exprt &e, std::map &result) { @@ -964,7 +964,8 @@ static void gather_symbol_live_ranges( } else { - var.length=std::max(var.length, (pc-var.start_pc)+1); + var.length = std::max( + var.length, static_cast((pc - var.start_pc) + 1)); } } } @@ -1136,7 +1137,8 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) // clang-format on PRECONDITION(!i_it->args.empty()); - auto target = numeric_cast_v(to_constant_expr(i_it->args[0])); + auto target = + numeric_cast_v(to_constant_expr(i_it->args[0])); targets.insert(target); a_entry.first->second.successors.push_back(target); @@ -1157,7 +1159,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) { if(is_label) { - auto target = numeric_cast_v(to_constant_expr(arg)); + auto target = numeric_cast_v(to_constant_expr(arg)); targets.insert(target); a_entry.first->second.successors.push_back(target); } @@ -2001,7 +2003,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) root, root_block, v.start_pc, - v.start_pc + v.length, + static_cast(v.start_pc + v.length), std::numeric_limits::max(), address_map); } @@ -2017,7 +2019,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) root, root_block, v.start_pc, - v.start_pc + v.length, + static_cast(v.start_pc + v.length), std::numeric_limits::max()); code_declt d(v.symbol_expr); block.statements().insert(block.statements().begin(), d); @@ -3172,7 +3174,7 @@ void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr( } } -std::vector +std::vector java_bytecode_convert_methodt::try_catch_handler( const method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) @@ -3211,7 +3213,7 @@ void java_bytecode_initialize_parameter_names( java_method_typet::parameterst ¶meters = method_type.parameters(); // Find number of parameters - unsigned slots_for_parameters = java_method_parameter_slots(method_type); + auto slots_for_parameters = java_method_parameter_slots(method_type); // Find parameter names in the local variable table: typedef std::pair base_name_and_identifiert; diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 2d12b5377bd..24012f10ca5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H #include "java_bytecode_convert_class.h" +#include "java_utils.h" #include #include @@ -74,8 +75,6 @@ class java_bytecode_convert_methodt convert(class_symbol, method, method_context); } - typedef uint16_t method_offsett; - protected: messaget log; symbol_table_baset &symbol_table; @@ -126,8 +125,8 @@ class java_bytecode_convert_methodt { public: symbol_exprt symbol_expr; - size_t start_pc; - size_t length; + method_offsett start_pc; + method_offsett length; bool is_parameter = false; std::vector holes; @@ -183,7 +182,7 @@ class java_bytecode_convert_methodt // return corresponding reference of variable const variablet &find_variable_for_slot( - size_t address, + method_offsett address, variablest &var_list); // JVM local variables @@ -193,7 +192,7 @@ class java_bytecode_convert_methodt NO_CAST }; - exprt variable(const exprt &arg, char type_char, size_t address); + exprt variable(const exprt &arg, char type_char, method_offsett address); // temporary variables std::list tmp_vars; diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index cd1544ef3c1..63ab1f43214 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +typedef uint16_t method_offsett; + struct java_bytecode_parse_treet { // Disallow copy construction and copy assignment, but allow move construction @@ -55,7 +57,7 @@ struct java_bytecode_parse_treet struct instructiont { source_locationt source_location; - unsigned address; + method_offsett address; u8 bytecode; typedef std::vector argst; argst args; @@ -112,9 +114,9 @@ struct java_bytecode_parse_treet { } - std::size_t start_pc; - std::size_t end_pc; - std::size_t handler_pc; + method_offsett start_pc; + method_offsett end_pc; + method_offsett handler_pc; struct_tag_typet catch_type; }; @@ -128,9 +130,9 @@ struct java_bytecode_parse_treet irep_idt name; std::string descriptor; std::optional signature; - std::size_t index; - std::size_t start_pc; - std::size_t length; + method_offsett index; + method_offsett start_pc; + method_offsett length; }; typedef std::vector local_variable_tablet; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index c1f5a383aac..b1c2b38a634 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -923,7 +923,7 @@ void java_bytecode_parsert::rbytecode(std::vector &instructions) instructions.emplace_back(); instructiont &instruction=instructions.back(); instruction.bytecode = bytecode; - instruction.address=start_of_instruction; + instruction.address=static_cast(start_of_instruction); instruction.source_location .set_java_bytecode_index(std::to_string(bytecode_index)); @@ -1604,7 +1604,7 @@ void java_bytecode_parsert::rinner_classes_attribute( classt &parsed_class = parse_tree.parsed_class; std::string name = parsed_class.name.c_str(); const u2 number_of_classes = read(); - const u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2; + const u4 number_of_bytes_to_be_read = static_cast(number_of_classes * 8 + 2); INVARIANT( number_of_bytes_to_be_read == attribute_length, "The number of bytes to be read for the InnerClasses attribute does not " diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index c64436d8c0b..51742b77f60 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -27,9 +27,9 @@ template struct procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, - java_bytecode_convert_methodt::method_offsett> + method_offsett> : public grapht< - cfg_base_nodet> + cfg_base_nodet> { typedef grapht< cfg_base_nodet> @@ -51,7 +51,7 @@ struct procedure_local_cfg_baset< for(const auto &inst : amap) { // Map instruction PCs onto node indices: - entry_map[inst.first]=this->add_node(); + entry_map[inst.first] = static_cast(this->add_node()); // Map back: (*this)[entry_map[inst.first]].PC=inst.first; } @@ -238,14 +238,13 @@ static bool is_store_to_slot( /// \param [out] var: A hole is added to `var`, unless it would be of zero size static void maybe_add_hole( local_variable_with_holest &var, - java_bytecode_convert_methodt::method_offsett from, - java_bytecode_convert_methodt::method_offsett to) + method_offsett from, + method_offsett to) { PRECONDITION(to>=from); if(to!=from) var.holes.push_back( - {from, - static_cast(to - from)}); + {from, static_cast(to - from)}); } /// See above @@ -262,10 +261,17 @@ static void populate_variable_address_map( { for(auto it=firstvar, itend=varlimit; it!=itend; ++it) { - if(it->var.start_pc+it->var.length>live_variable_at_address.size()) - live_variable_at_address.resize(it->var.start_pc+it->var.length); + if( + static_cast(it->var.start_pc + it->var.length) > + live_variable_at_address.size()) + { + live_variable_at_address.resize( + static_cast(it->var.start_pc + it->var.length)); + } - for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length; + for(method_offsett idx = it->var.start_pc, + idxlim = static_cast( + it->var.start_pc + it->var.length); idx != idxlim; ++idx) { @@ -332,7 +338,8 @@ static void populate_predecessor_map( #endif // Find the last instruction within the live range: - const auto end_pc = it->var.start_pc + it->var.length; + const auto end_pc = + static_cast(it->var.start_pc + it->var.length); auto amapit=amap.find(end_pc); INVARIANT( amapit!=amap.begin(), @@ -445,22 +452,20 @@ static void populate_predecessor_map( /// \return Returns the bytecode address of the closest common dominator of all /// given variable table entries. In the worst case the function entry point /// should always satisfy this criterion. -static java_bytecode_convert_methodt::method_offsett get_common_dominator( +static method_offsett get_common_dominator( const std::set &merge_vars, const java_cfg_dominatorst &dominator_analysis) { PRECONDITION(!merge_vars.empty()); - auto first_pc = - std::numeric_limits::max(); + auto first_pc = std::numeric_limits::max(); for(auto v : merge_vars) { if(v->var.start_pcvar.start_pc; } - std::vector - candidate_dominators; + std::vector candidate_dominators; for(auto v : merge_vars) { const auto &dominator_nodeidx= @@ -507,7 +512,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator( static void populate_live_range_holes( local_variable_with_holest &merge_into, const std::set &merge_vars, - java_bytecode_convert_methodt::method_offsett expanded_live_range_start) + method_offsett expanded_live_range_start) { std::vector sorted_by_startpc( merge_vars.begin(), merge_vars.end()); @@ -555,16 +560,17 @@ static void merge_variable_table_entries( // as it was not visible in the original local variable table) populate_live_range_holes(merge_into, merge_vars, found_dominator); - java_bytecode_convert_methodt::method_offsett last_pc = 0; + method_offsett last_pc = 0; for(auto v : merge_vars) { - if(v->var.start_pc+v->var.length>last_pc) - last_pc=v->var.start_pc+v->var.length; + if(static_cast(v->var.start_pc + v->var.length) > last_pc) + last_pc = static_cast(v->var.start_pc + v->var.length); } // Apply the changes: merge_into.var.start_pc=found_dominator; - merge_into.var.length=last_pc-found_dominator; + merge_into.var.length = + static_cast(last_pc - found_dominator); #ifdef DEBUG debug_out << "Merged " << merge_vars.size() << " variables named " @@ -850,7 +856,7 @@ void java_bytecode_convert_methodt::setup_local_variables( /// nothing covers `address`. const java_bytecode_convert_methodt::variablet & java_bytecode_convert_methodt::find_variable_for_slot( - size_t address, + method_offsett address, variablest &var_list) { for(const variablet &var : var_list) diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index a851c2f27f6..773d88e8131 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -144,12 +144,13 @@ unsigned java_local_variable_slots(const typet &t) return bitwidth == 64 ? 2u : 1u; } -unsigned java_method_parameter_slots(const java_method_typet &t) +method_offsett java_method_parameter_slots(const java_method_typet &t) { - unsigned slots=0; + method_offsett slots = 0; for(const auto &p : t.parameters()) - slots+=java_local_variable_slots(p.type()); + slots = + static_cast(slots + java_local_variable_slots(p.type())); return slots; } diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 4deb6183cde..5e21f8e085d 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -83,7 +83,7 @@ unsigned java_local_variable_slots(const typet &t); /// Returns the the number of JVM local variables (slots) used by the JVM to /// pass, upon call, the arguments of a Java method whose type is \p t. -unsigned java_method_parameter_slots(const java_method_typet &t); +method_offsett java_method_parameter_slots(const java_method_typet &t); const std::string java_class_to_package(const std::string &canonical_classname); From 9c4aec879dd86199badb4b285da63ca0efc5a54f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Jul 2018 10:30:26 +0100 Subject: [PATCH 13/18] Use non-truncating cast of constant expressions --- src/ansi-c/c_preprocess.cpp | 3 ++- src/goto-cc/ms_cl_cmdline.cpp | 14 +++++++------- src/goto-cc/ms_link_cmdline.cpp | 9 +++++---- src/solvers/smt2/smt2_tokenizer.cpp | 6 ++++++ src/util/config.cpp | 6 ++++++ 5 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index afe51b01010..b1823aa6060 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -253,7 +253,8 @@ bool c_preprocess_visual_studio( // This marks the command file as UTF-8, which Visual Studio // understands. - command_file << char(0xef) << char(0xbb) << char(0xbf); + command_file << (unsigned char)0xefu << (unsigned char)0xbbu + << (unsigned char)0xbfu; command_file << "/nologo" << '\n'; command_file << "/E" << '\n'; diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index fe4edcf1295..c892275970c 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/src/goto-cc/ms_cl_cmdline.cpp @@ -182,9 +182,9 @@ void ms_cl_cmdlinet::process_response_file(const std::string &file) // these may be Unicode -- which is indicated by 0xff 0xfe std::string line; getline(infile, line); - if(line.size()>=2 && - line[0]==static_cast(0xff) && - line[1]==static_cast(0xfe)) + if( + line.size() >= 2 && static_cast(line[0]) == 0xffu && + static_cast(line[1]) == 0xfeu) { // Unicode, UTF-16 little endian @@ -208,10 +208,10 @@ void ms_cl_cmdlinet::process_response_file(const std::string &file) #endif } - else if(line.size()>=3 && - line[0]==static_cast(0xef) && - line[1]==static_cast(0xbb) && - line[2]==static_cast(0xbf)) + else if( + line.size() >= 3 && static_cast(line[0]) == 0xefu && + static_cast(line[1]) == 0xbbu && + static_cast(line[2]) == 0xbfu) { // This is the UTF-8 BOM. We can proceed as usual, since // we use UTF-8 internally. diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp index bbb9a3348c1..6ba05622219 100644 --- a/src/goto-cc/ms_link_cmdline.cpp +++ b/src/goto-cc/ms_link_cmdline.cpp @@ -120,8 +120,8 @@ void ms_link_cmdlinet::process_response_file(const std::string &file) std::string line; getline(infile, line); if( - line.size() >= 2 && line[0] == static_cast(0xff) && - line[1] == static_cast(0xfe)) + line.size() >= 2 && static_cast(line[0]) == 0xffu && + static_cast(line[1]) == 0xfeu) { // Unicode, UTF-16 little endian @@ -146,8 +146,9 @@ void ms_link_cmdlinet::process_response_file(const std::string &file) #endif } else if( - line.size() >= 3 && line[0] == static_cast(0xef) && - line[1] == static_cast(0xbb) && line[2] == static_cast(0xbf)) + line.size() >= 3 && static_cast(line[0]) == 0xefu && + static_cast(line[1]) == 0xbbu && + static_cast(line[2]) == 0xbfu) { // This is the UTF-8 BOM. We can proceed as usual, since // we use UTF-8 internally. diff --git a/src/solvers/smt2/smt2_tokenizer.cpp b/src/solvers/smt2/smt2_tokenizer.cpp index 6272bb8d5a8..63d8e1e0bcb 100644 --- a/src/solvers/smt2/smt2_tokenizer.cpp +++ b/src/solvers/smt2/smt2_tokenizer.cpp @@ -223,7 +223,13 @@ void smt2_tokenizert::get_token_from_stream() case ' ': case '\r': case '\t': +#include +#ifdef _MSC_VER +#pragma warning(disable : 4309) + // truncation of constant value +#endif case static_cast(160): // non-breaking space +#include // skip any whitespace break; diff --git a/src/util/config.cpp b/src/util/config.cpp index 49afdc2e3d3..f5f0e473cdd 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1120,10 +1120,16 @@ bool configt::set(const cmdlinet &cmdline) INVARIANT( ansi_c.double_width == sizeof(double) * CHAR_BIT, "double width shall be equal to the system double width"); +#include +#ifdef _MSC_VER +#pragma warning(disable : 4309) +// truncation of constant value +#endif INVARIANT( ansi_c.char_is_unsigned == (static_cast((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1), "char_is_unsigned flag shall indicate system char unsignedness"); +#include #ifndef _WIN32 // On Windows, long double width varies by compiler From 825e0e6acfebffc964d611cfc138f066919bd352 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Jul 2018 10:30:11 +0100 Subject: [PATCH 14/18] Silence Visual Studio warnings about non-thread-safe static objects --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 8 ++++++++ jbmc/src/java_bytecode/java_entry_point.cpp | 10 +++++++++- jbmc/src/java_bytecode/java_utils.cpp | 8 ++++++++ jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ++++++++ src/analyses/reaching_definitions.cpp | 8 ++++++++ src/goto-instrument/wmm/event_graph.h | 8 ++++++++ src/solvers/sat/satcheck_minisat2.cpp | 6 ++++++ src/util/irep.cpp | 10 ++++++++++ src/util/string_container.h | 8 ++++++++ 9 files changed, 73 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index db24a2579c0..5f78a7d8251 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -65,7 +65,15 @@ ci_lazy_methodst::ci_lazy_methodst( /// class static bool references_class_model(const exprt &expr) { +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static const struct_tag_typet class_type("java::java.lang.Class"); +#ifdef _MSC_VER +#include +#endif for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it) { diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fa074554c8e..c39b94a8bf7 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -76,9 +76,17 @@ static bool should_init_symbol(const symbolt &sym) irep_idt get_java_class_literal_initializer_signature() { - static irep_idt signature = +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif + static const irep_idt signature = "java::java.lang.Class.cproverInitializeClassLiteral:" "(Ljava/lang/String;ZZZZZZZ)V"; +#ifdef _MSC_VER +#include +#endif return signature; } diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 773d88e8131..3e5163aafef 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -519,9 +519,17 @@ get_inherited_component( /// \return true if this static field is known never to be null bool is_non_null_library_global(const irep_idt &symbolid) { +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static const irep_idt in = "java::java.lang.System.in"; static const irep_idt out = "java::java.lang.System.out"; static const irep_idt err = "java::java.lang.System.err"; +#ifdef _MSC_VER +#include +#endif return symbolid == in || symbolid == out || symbolid == err; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 7ed4105af63..3d48abe0347 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -917,7 +917,15 @@ bool jbmc_parse_optionst::process_goto_functions( bool jbmc_parse_optionst::can_generate_function_body(const irep_idt &name) { +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static const irep_idt initialize_id = INITIALIZE_FUNCTION; +#ifdef _MSC_VER +#include +#endif return name != goto_functionst::entry_point() && name != initialize_id; } diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index f44562ed90f..dea307b6d49 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -723,7 +723,15 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get( { populate_cache(identifier); +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static ranges_at_loct empty; +#ifdef _MSC_VER +#include +#endif export_cachet::const_iterator entry=export_cache.find(identifier); diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h index 5f4acaa338d..31135d1aa17 100644 --- a/src/goto-instrument/wmm/event_graph.h +++ b/src/goto-instrument/wmm/event_graph.h @@ -348,7 +348,15 @@ class event_grapht std::list* initial_filtering(std::list* order) { +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static std::list new_order; +#ifdef _MSC_VER +#include +#endif /* intersection */ for(const auto &evt : *order) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 633d4f1ff8a..a3247ec2b2e 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -18,8 +18,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#ifdef _MSC_VER +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif #include #include +#include #ifndef l_False # define l_False Minisat::l_False diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 36e103ea8ff..36b5fa135be 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -48,7 +48,17 @@ const irep_idt &irept::get(const irep_idt &name) const if(it==s.end()) { +#ifdef _MSC_VER +// NOLINTNEXTLINE(build/include) +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static const irep_idt empty; +#ifdef _MSC_VER +// NOLINTNEXTLINE(build/include) +#include +#endif return empty; } return it->second.id(); diff --git a/src/util/string_container.h b/src/util/string_container.h index 10d2ea4d3e6..411a9c6c1c2 100644 --- a/src/util/string_container.h +++ b/src/util/string_container.h @@ -110,7 +110,15 @@ class string_containert /// Get a reference to the global string container. inline string_containert &get_string_container() { +#ifdef _MSC_VER +#include +#pragma warning(disable:4640) + // construction of local static object is not thread-safe +#endif static string_containert ret; +#ifdef _MSC_VER +#include +#endif return ret; } From 86ad618c6509bfe350254f6b268fc52426425dc3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 13 Nov 2018 07:59:44 +0000 Subject: [PATCH 15/18] Avoid spurious warning about hiding base class functions cmdlinet::parse has a different signature and we don't override it here. As an alternative option, we could rename functions. --- src/goto-cc/ms_cl_cmdline.h | 1 + src/goto-cc/ms_link_cmdline.h | 1 + 2 files changed, 2 insertions(+) diff --git a/src/goto-cc/ms_cl_cmdline.h b/src/goto-cc/ms_cl_cmdline.h index 28059a24b8d..cc773c12ea4 100644 --- a/src/goto-cc/ms_cl_cmdline.h +++ b/src/goto-cc/ms_cl_cmdline.h @@ -33,6 +33,7 @@ class ms_cl_cmdlinet:public goto_cc_cmdlinet void process_cl_option(const std::string &s); void process_response_file(const std::string &file); void process_response_file_line(const std::string &line); + using cmdlinet::parse; bool parse(const std::vector &); }; diff --git a/src/goto-cc/ms_link_cmdline.h b/src/goto-cc/ms_link_cmdline.h index 95390ff3bc1..f50fb0eb190 100644 --- a/src/goto-cc/ms_link_cmdline.h +++ b/src/goto-cc/ms_link_cmdline.h @@ -31,6 +31,7 @@ class ms_link_cmdlinet : public goto_cc_cmdlinet void process_link_option(const std::string &s); void process_response_file(const std::string &file); void process_response_file_line(const std::string &line); + using cmdlinet::parse; bool parse(const std::vector &); }; From abebf052e0053f82fea488e12d8200b49409bfad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Jan 2019 21:34:49 +0000 Subject: [PATCH 16/18] Avoid evaluation-order warnings with Visual Studio Constructing the arguments in place triggers a warning with Visual Studio. Just construct them in a fixed order upfront and move each of them. --- src/analyses/ai.cpp | 14 ++- .../unreachable_instructions.cpp | 8 +- src/goto-checker/properties.cpp | 9 +- src/goto-checker/properties.h | 2 +- src/goto-diff/goto_diff_base.cpp | 4 +- src/goto-programs/loop_ids.cpp | 8 +- .../show_goto_functions_json.cpp | 3 +- src/goto-programs/show_properties.cpp | 15 ++- src/goto-programs/show_symbol_table.cpp | 101 +++++++++++------- 9 files changed, 102 insertions(+), 62 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 3fd897c0d14..0eba7098566 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -95,11 +95,15 @@ jsont ai_baset::output_json( std::ostringstream out; i_it->output(out); - json_objectt location{ - {"locationNumber", json_numbert(std::to_string(i_it->location_number))}, - {"sourceLocation", json_stringt(i_it->source_location().as_string())}, - {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)}, - {"instruction", json_stringt(out.str())}}; + json_numbert location_number_json(std::to_string(i_it->location_number)); + json_stringt source_location_json(i_it->source_location.as_string()); + jsont abstract_state_json(abstract_state_before(i_it)->output_json(*this, ns)); + json_stringt instruction_json(out.str()); + json_objectt location( + {{"locationNumber", std::move(location_number_json)}, + {"sourceLocation", std::move(source_location_json)}, + {"abstractState", std::move(abstract_state_json)}, + {"instruction", std::move(instruction_json)}}); contents.push_back(std::move(location)); } diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 5f0cc4b8fff..d0541ea010a 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -151,9 +151,11 @@ static void add_to_json( s.erase(s.size()-1); // print info for file actually with full path - const source_locationt &l = it->second->source_location(); - json_objectt i_entry{{"sourceLocation", json(l)}, - {"statement", json_stringt(s)}}; + const source_locationt &l=it->second->source_location; + jsont source_location_json(json(l)); + json_stringt statement_json(s); + json_objectt i_entry{ + {{"sourceLocation", std::move(source_location_json)}, {"statement", std::move(statement_json)}}}; dead_ins.push_back(std::move(i_entry)); } diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 676b75efdae..e94a503b610 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -61,9 +61,9 @@ std::string as_string(property_statust status) property_infot::property_infot( goto_programt::const_targett pc, - std::string description, + const std::string &description, property_statust status) - : pc(pc), description(std::move(description)), status(status) + : pc(pc), description(description), status(status) { } @@ -93,9 +93,8 @@ void update_properties_from_goto_model( id2string(i_it->source_location().get_comment()); if(description.empty()) description = "assertion"; - properties.emplace( - i_it->source_location().get_property_id(), - property_infot{i_it, description, property_statust::NOT_CHECKED}); + property_infot info{i_it, description, property_statust::NOT_CHECKED}; + properties.emplace(i_it->source_location.get_property_id(), std::move(info)); } } } diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h index 9a74b700fd3..b4189beca50 100644 --- a/src/goto-checker/properties.h +++ b/src/goto-checker/properties.h @@ -59,7 +59,7 @@ struct property_infot { property_infot( goto_programt::const_targett pc, - std::string description, + const std::string &description, property_statust status); /// A pointer to the corresponding goto instruction diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 66872711d00..a8777bf6e5d 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -38,9 +38,9 @@ void goto_difft::output_functions() const } case ui_message_handlert::uit::JSON_UI: { + json_stringt total_number_of_functions_json{std::to_string(total_functions_count)}; json_objectt json_result{ - {"totalNumberOfFunctions", - json_stringt(std::to_string(total_functions_count))}}; + {{"totalNumberOfFunctions", std::move(total_number_of_functions_json)}}}; convert_function_group_json( json_result["newFunctions"].make_array(), new_functions, goto_model2); convert_function_group_json( diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index e3658577b91..53d21f1d2e1 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -85,9 +85,11 @@ void show_loop_ids_json( std::string id = id2string(goto_programt::loop_id(function_id, instruction)); - loops.push_back(json_objectt( - {{"name", json_stringt(id)}, - {"sourceLocation", json(instruction.source_location())}})); + json_stringt name_json{id}; + jsont source_location_json{json(it->source_location)}; + loops.push_back( + json_objectt{{{"name", std::move(name_json)}, + {"sourceLocation", std::move(source_location_json)}}}); } } } diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index eb2b2c8443e..3578c349d49 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -61,8 +61,9 @@ json_objectt show_goto_functions_jsont::convert( for(const goto_programt::instructiont &instruction : function.body.instructions) { + json_stringt instruction_id{instruction.to_string()}; json_objectt instruction_entry{ - {"instructionId", json_stringt(instruction.to_string())}}; + {{"instructionId", std::move(instruction_id)}}}; if(instruction.code().source_location().is_not_nil()) { diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index c3e94c26600..4d8f8c66664 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -143,12 +143,17 @@ void convert_properties_json( irep_idt property_id=source_location.get_property_id(); + json_stringt name_json{property_id}; + json_stringt class_json{property_class}; + jsont source_location_json{json(source_location)}; + json_stringt description_json{description}; + json_stringt expression_json{from_expr(ns, identifier, ins.guard)}; json_objectt json_property{ - {"name", json_stringt(property_id)}, - {"class", json_stringt(property_class)}, - {"sourceLocation", json(source_location)}, - {"description", json_stringt(description)}, - {"expression", json_stringt(from_expr(ns, identifier, ins.condition()))}}; + {{"name", std::move(name_json)}, + {"class", std::move(class_json)}, + {"sourceLocation", std::move(source_location_json)}, + {"description", std::move(description_json)}, + {"expression", std::move(expression_json)}}}; const irept &basic_block_lines = source_location.get_basic_block_source_lines(); diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 4a5b870ab60..0acf07929af 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -165,36 +165,59 @@ static void show_symbol_table_json_ui( if(symbol.value.is_not_nil()) ptr->from_expr(symbol.value, value_str, ns); + json_stringt pretty_name_json{symbol.pretty_name}; + json_stringt name_json{symbol.name}; + json_stringt base_name_json{symbol.base_name}; + json_stringt mode_json{symbol.mode}; + json_stringt module_json{symbol.module}; + json_stringt pretty_type_json{type_str}; + json_stringt pretty_value_json{value_str}; + jsont type_json{irep_converter.convert_from_irep(symbol.type)}; + jsont value_json{irep_converter.convert_from_irep(symbol.value)}; + jsont location_json{irep_converter.convert_from_irep(symbol.location)}; + jsont is_type_json{jsont::json_boolean(symbol.is_type)}; + jsont is_macro_json{jsont::json_boolean(symbol.is_macro)}; + jsont is_exported_json{jsont::json_boolean(symbol.is_exported)}; + jsont is_input_json{jsont::json_boolean(symbol.is_input)}; + jsont is_output_json{jsont::json_boolean(symbol.is_output)}; + jsont is_state_var_json{jsont::json_boolean(symbol.is_state_var)}; + jsont is_property_json{jsont::json_boolean(symbol.is_property)}; + jsont is_static_lifetime_json{jsont::json_boolean(symbol.is_static_lifetime)}; + jsont is_thread_local_json{jsont::json_boolean(symbol.is_thread_local)}; + jsont is_lvalue_json{jsont::json_boolean(symbol.is_lvalue)}; + jsont is_file_local_json{jsont::json_boolean(symbol.is_file_local)}; + jsont is_extern_json{jsont::json_boolean(symbol.is_extern)}; + jsont is_volatile_json{jsont::json_boolean(symbol.is_volatile)}; + jsont is_parameter_json{jsont::json_boolean(symbol.is_parameter)}; + jsont is_auxiliary_json{jsont::json_boolean(symbol.is_auxiliary)}; + jsont is_weak_json{jsont::json_boolean(symbol.is_weak)}; json_objectt symbol_json{ - {"prettyName", json_stringt(symbol.pretty_name)}, - {"name", json_stringt(symbol.name)}, - {"baseName", json_stringt(symbol.base_name)}, - {"mode", json_stringt(symbol.mode)}, - {"module", json_stringt(symbol.module)}, - - {"prettyType", json_stringt(type_str)}, - {"prettyValue", json_stringt(value_str)}, - - {"type", irep_converter.convert_from_irep(symbol.type)}, - {"value", irep_converter.convert_from_irep(symbol.value)}, - {"location", irep_converter.convert_from_irep(symbol.location)}, - - {"isType", jsont::json_boolean(symbol.is_type)}, - {"isMacro", jsont::json_boolean(symbol.is_macro)}, - {"isExported", jsont::json_boolean(symbol.is_exported)}, - {"isInput", jsont::json_boolean(symbol.is_input)}, - {"isOutput", jsont::json_boolean(symbol.is_output)}, - {"isStateVar", jsont::json_boolean(symbol.is_state_var)}, - {"isProperty", jsont::json_boolean(symbol.is_property)}, - {"isStaticLifetime", jsont::json_boolean(symbol.is_static_lifetime)}, - {"isThreadLocal", jsont::json_boolean(symbol.is_thread_local)}, - {"isLvalue", jsont::json_boolean(symbol.is_lvalue)}, - {"isFileLocal", jsont::json_boolean(symbol.is_file_local)}, - {"isExtern", jsont::json_boolean(symbol.is_extern)}, - {"isVolatile", jsont::json_boolean(symbol.is_volatile)}, - {"isParameter", jsont::json_boolean(symbol.is_parameter)}, - {"isAuxiliary", jsont::json_boolean(symbol.is_auxiliary)}, - {"isWeak", jsont::json_boolean(symbol.is_weak)}}; + {{"prettyName", std::move(pretty_name_json)}, + {"name", std::move(name_json)}, + {"baseName", std::move(base_name_json)}, + {"mode", std::move(mode_json)}, + {"module", std::move(module_json)}, + {"prettyType", std::move(pretty_type_json)}, + {"prettyValue", std::move(pretty_value_json)}, + {"type", std::move(type_json)}, + {"value", std::move(value_json)}, + {"location", std::move(location_json)}, + {"isType", std::move(is_type_json)}, + {"isMacro", std::move(is_macro_json)}, + {"isExported", std::move(is_exported_json)}, + {"isInput", std::move(is_input_json)}, + {"isOutput", std::move(is_output_json)}, + {"isStateVar", std::move(is_state_var_json)}, + {"isProperty", std::move(is_property_json)}, + {"isStaticLifetime", std::move(is_static_lifetime_json)}, + {"isThreadLocal", std::move(is_thread_local_json)}, + {"isLvalue", std::move(is_lvalue_json)}, + {"isFileLocal", std::move(is_file_local_json)}, + {"isExtern", std::move(is_extern_json)}, + {"isVolatile", std::move(is_volatile_json)}, + {"isParameter", std::move(is_parameter_json)}, + {"isAuxiliary", std::move(is_auxiliary_json)}, + {"isWeak", std::move(is_weak_json)}}}; result.push_back(id2string(symbol.name), std::move(symbol_json)); } @@ -224,15 +247,19 @@ static void show_symbol_table_brief_json_ui( if(symbol.type.is_not_nil()) ptr->from_type(symbol.type, type_str, ns); + json_stringt pretty_name_json{symbol.pretty_name}; + json_stringt base_name_json{symbol.base_name}; + json_stringt mode_json{symbol.mode}; + json_stringt module_json{symbol.module}; + json_stringt pretty_type_json{type_str}; + jsont type_json{irep_converter.convert_from_irep(symbol.type)}; json_objectt symbol_json{ - {"prettyName", json_stringt(symbol.pretty_name)}, - {"baseName", json_stringt(symbol.base_name)}, - {"mode", json_stringt(symbol.mode)}, - {"module", json_stringt(symbol.module)}, - - {"prettyType", json_stringt(type_str)}, - - {"type", irep_converter.convert_from_irep(symbol.type)}}; + {{"prettyName", std::move(pretty_name_json)}, + {"baseName", std::move(base_name_json)}, + {"mode", std::move(mode_json)}, + {"module", std::move(module_json)}, + {"prettyType", std::move(pretty_type_json)}, + {"type", std::move(type_json)}}}; result.push_back(id2string(symbol.name), std::move(symbol_json)); } From 85155f1bab04316e292c88696a89fd3230784eea Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Jun 2018 10:02:49 +0000 Subject: [PATCH 17/18] Visual Studio: Enable all warnings other than deprecation and make them errors Treat all Visual Studio warnings except those that we cannot do anything about as errors. --- src/config.inc | 48 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 47 insertions(+), 1 deletion(-) diff --git a/src/config.inc b/src/config.inc index f7f7b9f54a9..69428c99672 100644 --- a/src/config.inc +++ b/src/config.inc @@ -3,7 +3,53 @@ BUILD_ENV = AUTO # Enable all warnings and treat them as errors ifeq ($(BUILD_ENV),MSVC) - #CXXFLAGS += /Wall /WX + CXXFLAGS += /Wall /WX + # disable warning "decorated name length exceeded" + CXXFLAGS += /wd4503 + # disable deprecation warnings + CXXFLAGS += /wd4996 + # disable warning "unreferenced inline function has been removed" + CXXFLAGS += /wd4514 + # disable warning "padding added after data member" + CXXFLAGS += /wd4820 + # disable warning "function not inlined" + CXXFLAGS += /wd4710 + # disable warning "layout of class may have changed from a previous version of + # the compiler due to better packing of member" + CXXFLAGS += /wd4371 /wd4435 + # disable warning "conditional expression is constant" + CXXFLAGS += /wd4127 + # disable warning "behavior change ... called instead of ..." + CXXFLAGS += /wd4350 + # disable warning "assignment operator could not be generated" + CXXFLAGS += /wd4512 /wd4626 + # disable warning "default/copy constructor could not be generated" + CXXFLAGS += /wd4623 /wd4510 /wd4625 /wd4610 + # disable warning "no override available, function is hidden" + CXXFLAGS += /wd4266 + # disable warning "unreferenced local function has been removed" + CXXFLAGS += /wd4505 + # disable warning "'this' used in base member initializer list" - which would + # be useful to have, but it's not always clear where to put a silencing pragma + CXXFLAGS += /wd4355 + # disable warning "#pragma warning(pop): likely mismatch, popping warning + # state pushed in different file" + CXXFLAGS += /wd5031 /wd5032 + # disable warning "move constructor/assignment operator was implicitly defined + # as deleted" + CXXFLAGS += /wd5026 /wd5027 + # disable warning "Informational: catch(...) semantics changed since Visual + # C++ 7.1; structured exceptions (SEH) are no longer caught" + CXXFLAGS += /wd4571 + # disable warning "Compiler will insert Spectre mitigation with /Qspectre" + CXXFLAGS += /wd5045 + # disable warning "signed/unsigned mismatch" as VS2017 STL headers yield it + # CXXFLAGS += /wd4365 + # disable warning "format string expected is not a string literal" as VS2017 STL headers yield it + CXXFLAGS += /wd4774 + # disable warning "#pragma warning: there is no warning number '...'" to + # support multiple Visual Studio versions + CXXFLAGS += /wd4619 else CXXFLAGS += -Wall -pedantic -Werror -Wswitch-enum CXXFLAGS += -Wno-deprecated-declarations From 0ca98d234ce7aa44d7919bc30bcc9b5fc2e93d8a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Jul 2018 17:24:46 +0100 Subject: [PATCH 18/18] Enable additional warnings with GCC/Clang to match Visual Studio --- CMakeLists.txt | 5 ++++- src/config.inc | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2c1289a121e..808681d6d8d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -78,6 +78,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") # Enable lots of warnings set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum \ + -Wextra -Wconversion \ -Wno-deprecated-declarations -Wno-maybe-uninitialized") elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") @@ -86,7 +87,9 @@ elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") # Enable lots of warnings set(CMAKE_CXX_FLAGS - "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum -Wno-deprecated-declarations") + "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum \ + -Wextra -Wconversion \ + -Wno-deprecated-declarations") elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") # This would be the place to enable warnings for Windows builds, although # config.inc doesn't seem to do that currently diff --git a/src/config.inc b/src/config.inc index 69428c99672..c5d09cff528 100644 --- a/src/config.inc +++ b/src/config.inc @@ -52,7 +52,7 @@ ifeq ($(BUILD_ENV),MSVC) CXXFLAGS += /wd4619 else CXXFLAGS += -Wall -pedantic -Werror -Wswitch-enum - CXXFLAGS += -Wno-deprecated-declarations + CXXFLAGS += -Wno-deprecated-declarations -Wextra -Wconversion # GCC only, silence clang warning CXXFLAGS += -Wno-maybe-uninitialized -Wno-unknown-warning-option endif