Fix various type conversion and deprecation warnings reported by Visual studio

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

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 <util/pragma_push.def>
+#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 <util/pragma_pop.def>
+#endif
 
   for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
   {

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());

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<std::size_t>(to_constant_expr(arg));
@@ -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<std::size_t>(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<std::size_t>(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<std::size_t>(child_offset)].swap(newlabel);
 
   // Perform the same transformation on the index tree:
   block_tree_nodet newnode;
@@ -932,18 +932,17 @@ 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<std::size_t>(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<std::size_t>(child_offset)])
+      .code());
 }
 
 static void gather_symbol_live_ranges(
-  java_bytecode_convert_methodt::method_offsett pc,
+  method_offsett pc,
   const exprt &e,
   std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
 {
@@ -965,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<method_offsett>((pc - var.start_pc) + 1));
       }
     }
   }
@@ -1137,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<unsigned>(to_constant_expr(i_it->args[0]));
+      auto target =
+        numeric_cast_v<method_offsett>(to_constant_expr(i_it->args[0]));
       targets.insert(target);
 
       a_entry.first->second.successors.push_back(target);
@@ -1158,7 +1159,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       {
         if(is_label)
         {
-          auto target = numeric_cast_v<unsigned>(to_constant_expr(arg));
+          auto target = numeric_cast_v<method_offsett>(to_constant_expr(arg));
           targets.insert(target);
           a_entry.first->second.successors.push_back(target);
         }
@@ -2002,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<method_offsett>(v.start_pc + v.length),
       std::numeric_limits<method_offsett>::max(),
       address_map);
   }
@@ -2018,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<method_offsett>(v.start_pc + v.length),
       std::numeric_limits<method_offsett>::max());
     code_declt d(v.symbol_expr);
     block.statements().insert(block.statements().begin(), d);
@@ -3173,7 +3174,7 @@ void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(
   }
 }
 
-std::vector<java_bytecode_convert_methodt::method_offsett>
+std::vector<method_offsett>
 java_bytecode_convert_methodt::try_catch_handler(
   const method_offsett address,
   const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)
@@ -3212,7 +3213,7 @@ void java_bytecode_initialize_parameter_names(
   java_method_typet::parameterst &parameters = 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<irep_idt, irep_idt> base_name_and_identifiert;

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
 
 #include "java_bytecode_convert_class.h"
+#include "java_utils.h"
 
 #include <util/expanding_vector.h>
 #include <util/message.h>
@@ -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<holet> 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<symbol_exprt> tmp_vars;

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 #include <set>
 
+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<exprt> 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<std::string> 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_variablet> local_variable_tablet;