Build with numeric conversion warnings enabled

tautschnig · tautschnig · commit ff85b540dae2 · 2025-02-07T12:32:24.000Z
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -77,7 +77,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
     #   Enable lots of warnings
     set(CMAKE_CXX_FLAGS
-        "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum \
+        "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wswitch-enum -Wconversion \
          -Wno-deprecated-declarations -Wno-maybe-uninitialized")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
        "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
@@ -86,7 +86,7 @@ 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 -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/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
@@ -163,7 +163,7 @@ bool symex_bmct::should_stop_unwind(
 
 bool symex_bmct::get_unwind_recursion(
   const irep_idt &id,
-  unsigned thread_nr,
+  std::size_t thread_nr,
   std::size_t unwind)
 {
   tvt abort_unwind_decision;
diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h
@@ -110,7 +110,7 @@ class symex_bmct : public goto_symext
 
   bool get_unwind_recursion(
     const irep_idt &identifier,
-    unsigned thread_nr,
+    std::size_t thread_nr,
     std::size_t unwind) override;
 
   symex_coveraget symex_coverage;
diff --git 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<unsigned> thread_nr;
+  std::optional<std::size_t> 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<irep_idt, unsigned>(id, *thread_nr)] = uw;
+      thread_loop_map[std::pair<irep_idt, std::size_t>(id, *thread_nr)] = uw;
     }
     else
     {
@@ -188,13 +188,13 @@ void unwindsett::parse_unwindset(
 }
 
 std::optional<unsigned>
-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<irep_idt, unsigned>(loop_id, thread_nr));
+    thread_loop_map.find(std::pair<irep_idt, std::size_t>(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
@@ -44,7 +44,7 @@ class unwindsett
 
   // queries
   std::optional<unsigned>
-  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::pair<irep_idt, unsigned>, std::optional<unsigned>>;
+    std::map<std::pair<irep_idt, std::size_t>, std::optional<unsigned>>;
   thread_loop_mapt thread_loop_map;
 
   void parse_unwindset_one_loop(
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
@@ -112,7 +112,7 @@ class goto_trace_stept
   goto_programt::const_targett pc;
 
   // this transition done by given thread number
-  unsigned thread_nr;
+  std::size_t thread_nr;
 
   // for assume, assert, goto
   bool cond_value;
diff --git 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 <cmath>
-
 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<int>(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
@@ -505,7 +505,7 @@ class goto_symext
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
-    unsigned thread_nr,
+    std::size_t thread_nr,
     std::size_t unwind);
 
   /// Iterates over \p arguments and assigns them to the parameters, which are
diff --git 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<unsigned, std::list<guardt> > a_s_r_entryt;
+  typedef std::pair<std::size_t, std::list<guardt> > a_s_r_entryt;
   typedef std::list<guardt> a_s_w_entryt;
   std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
   std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
diff --git 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<unsigned, event_listt> per_thread_mapt;
+  typedef std::map<std::size_t, event_listt> 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
@@ -78,7 +78,7 @@ void partial_order_concurrencyt::build_event_lists(
   add_init_writes(equation);
 
   // a per-thread counter
-  std::map<unsigned, unsigned> counter;
+  std::map<std::size_t, unsigned> 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
@@ -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
@@ -74,7 +74,7 @@ struct symex_level2t
   renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> 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
@@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "path_storage.h"
 #include "symex_assign.h"
 
-bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, std::size_t)
+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
@@ -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,8 +876,8 @@ 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()
+    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;
 
@@ -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,
diff --git 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<state.threads.size())
   {
-    unsigned t=state.source.thread_nr+1;
+    std::size_t t=state.source.thread_nr+1;
 #if 0
     std::cout << "********* Now executing thread " << t << '\n';
 #endif
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
@@ -35,7 +35,7 @@ class symex_targett
   /// first instruction of the input GOTO program.
   struct sourcet
   {
-    unsigned thread_nr;
+    std::size_t thread_nr;
     irep_idt function_id;
     // The program counter is an iterator which indicates where the execution
     // is in its program sequence
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
@@ -956,6 +956,7 @@ void float_bvt::normalization_shift(
   PRECONDITION(fraction_bits != 0);
 
   std::size_t depth = address_bits(fraction_bits - 1);
+  CHECK_RETURN(depth > 0);
 
   exponent = typecast_exprt(
     exponent, signedbv_typet(std::max(depth, exponent_bits + 1)));

Original file line number	Diff line number	Diff line change
`@@ -163,7 +163,7 @@ bool symex_bmct::should_stop_unwind(`
`163`	`163`
`164`	`164`	`bool symex_bmct::get_unwind_recursion(`
`165`	`165`	`const irep_idt &id,`
`166`		`- unsigned thread_nr,`
	`166`	`+ std::size_t thread_nr,`
`167`	`167`	`std::size_t unwind)`
`168`	`168`	`{`
`169`	`169`	`tvt abort_unwind_decision;`
Original file line number	Diff line number	Diff line change
`@@ -33,14 +33,14 @@ void unwindsett::parse_unwindset_one_loop(`
`33`	`33`	`if(val.empty())`
`34`	`34`	`return;`
`35`	`35`
`36`		`- std::optional<unsigned> thread_nr;`
	`36`	`+ std::optional<std::size_t> thread_nr;`
`37`	`37`	`if(isdigit(val[0]))`
`38`	`38`	`{`
`39`	`39`	`auto c_pos = val.find(':');`
`40`	`40`	`if(c_pos != std::string::npos)`
`41`	`41`	`{`
`42`	`42`	`std::string nr = val.substr(0, c_pos);`
`43`		`- thread_nr = unsafe_string2unsigned(nr);`
	`43`	`+ thread_nr = unsafe_string2size_t(nr);`
`44`	`44`	`val.erase(0, nr.size() + 1);`
`45`	`45`	`}`
`46`	`46`	`}`
`@@ -170,7 +170,7 @@ void unwindsett::parse_unwindset_one_loop(`
`170`	`170`
`171`	`171`	`if(thread_nr.has_value())`
`172`	`172`	`{`
`173`		`- thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;`
	`173`	`+ thread_loop_map[std::pair<irep_idt, std::size_t>(id, *thread_nr)] = uw;`
`174`	`174`	`}`
`175`	`175`	`else`
`176`	`176`	`{`
`@@ -188,13 +188,13 @@ void unwindsett::parse_unwindset(`
`188`	`188`	`}`
`189`	`189`
`190`	`190`	`std::optional<unsigned>`
`191`		`-unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const`
	`191`	`+unwindsett::get_limit(const irep_idt &loop_id, std::size_t thread_nr) const`
`192`	`192`	`{`
`193`	`193`	`// We use the most specific limit we have`
`194`	`194`
`195`	`195`	`// thread x loop`
`196`	`196`	`auto tl_it =`
`197`		`- thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));`
	`197`	`+ thread_loop_map.find(std::pair<irep_idt, std::size_t>(loop_id, thread_nr));`
`198`	`198`
`199`	`199`	`if(tl_it != thread_loop_map.end())`
`200`	`200`	`return tl_it->second;`