std::distance returns a signed type, wrap in explicit cast

Visual Studio warns about signed/unsigned conversion and limited range of types.

Author: tautschnig

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<exprt> &exprs, const irep_idt &id)
 {
   return std::count_if(

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<std::ptrdiff_t>(current_pos),
+    --tokens.end());
 }

src/goto-instrument/goto_program2code.cpp

@@ -1559,7 +1559,8 @@ void goto_program2codet::cleanup_code_block(
       operands.size()>1 && i<operands.size();
      ) // no ++i
   {
-    exprt::operandst::iterator it=operands.begin()+i;
+    exprt::operandst::iterator it =
+      operands.begin() + static_cast<std::ptrdiff_t>(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<std::ptrdiff_t>(i) + 1,
+          it->operands().begin(),
+          it->operands().end());
+        operands.erase(operands.begin() + static_cast<std::ptrdiff_t>(i));
         // no ++i
       }
       else

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<std::ptrdiff_t>(width));
 
   return bv;
 }

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<std::size_t>(index_as_int);
 
-  bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
+  bvt result_bv(
+    src_bv.begin() + static_cast<std::ptrdiff_t>(offset),
+    src_bv.begin() + static_cast<std::ptrdiff_t>(offset + bv_width));
 
   return result_bv;
 }

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<std::ptrdiff_t>(fraction_bits));
     }
 
     return bv;

src/solvers/flattening/boolbv_typecast.cpp

@@ -77,8 +77,8 @@ 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<std::ptrdiff_t>(src.size() / 2));
+      upper.assign(src.begin() + static_cast<std::ptrdiff_t>(src.size() / 2), src.end());
       type_conversion(
         to_complex_type(src_type).subtype(),
         lower,

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<std::ptrdiff_t>(sub_idx));
       std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op));
 
       if(subtype.id() == ID_floatbv)

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<std::ptrdiff_t>(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<std::ptrdiff_t>(result.size() - n));
 
   POSTCONDITION(result.size() == n);
   return result;

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<std::ptrdiff_t>(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<std::ptrdiff_t>(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<std::ptrdiff_t>(spec.f));
 
   // removes the sign
   exponent.resize(spec.e);