Merge pull request #1205 from tautschnig/sign-compare-fix

Avoid spurious signed/unsigned comparison warnings

Author: Daniel Kroening

src/symex/path_search.cpp

@@ -281,15 +281,15 @@ bool path_searcht::drop_state(const statet &state)
   }
 
   // depth limit
-  if(depth_limit>=0 && state.get_depth()>depth_limit)
+  if(state.get_depth()>=depth_limit)
     return true;
 
   // context bound
-  if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound)
+  if(state.get_no_thread_interleavings()>=context_bound)
     return true;
 
   // branch bound
-  if(branch_bound>=0 && state.get_no_branches()>branch_bound)
+  if(state.get_no_branches()>=branch_bound)
     return true;
 
   // unwinding limit -- loops
@@ -298,7 +298,7 @@ bool path_searcht::drop_state(const statet &state)
     bool stop=false;
 
     for(const auto &loop_info : state.unwinding_map)
-      if(loop_info.second>unwind_limit)
+      if(loop_info.second>=unwind_limit)
       {
         stop=true;
         break;
@@ -324,7 +324,7 @@ bool path_searcht::drop_state(const statet &state)
     bool stop=false;
 
     for(const auto &rec_info : state.recursion_map)
-      if(rec_info.second>unwind_limit)
+      if(rec_info.second>=unwind_limit)
       {
         stop=true;
         break;

src/symex/path_search.h

@@ -19,18 +19,20 @@ Author: Daniel Kroening, [email protected]
 
 #include <path-symex/path_symex_state.h>
 
+#include <limits>
+
 class path_searcht:public safety_checkert
 {
 public:
   explicit path_searcht(const namespacet &_ns):
     safety_checkert(_ns),
     show_vcc(false),
     eager_infeasibility(false),
-    depth_limit(-1), // no limit
-    context_bound(-1),
-    branch_bound(-1),
-    unwind_limit(-1),
-    time_limit(-1),
+    depth_limit(std::numeric_limits<unsigned>::max()),
+    context_bound(std::numeric_limits<unsigned>::max()),
+    branch_bound(std::numeric_limits<unsigned>::max()),
+    unwind_limit(std::numeric_limits<unsigned>::max()),
+    time_limit(std::numeric_limits<unsigned>::max()),
     search_heuristic(search_heuristict::DFS)
   {
   }
@@ -132,11 +134,11 @@ class path_searcht:public safety_checkert
   void initialize_property_map(
     const goto_functionst &goto_functions);
 
-  int depth_limit;
-  int context_bound;
-  int branch_bound;
-  int unwind_limit;
-  int time_limit;
+  unsigned depth_limit;
+  unsigned context_bound;
+  unsigned branch_bound;
+  unsigned unwind_limit;
+  unsigned time_limit;
 
   enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;