Explicit type cast to avoid signed/unsigned warning

NathanJPhillips · Jul 7, 2018 · 96a7014 · 96a7014
1 parent 8187bdd
commit 96a7014
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h
@@ -15,7 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/irep.h>
 
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
-#define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max()
+#define MAX_NONDET_STRING_LENGTH \
+  static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max())
 #define MAX_NONDET_TREE_DEPTH 5
 #define MAX_NONNULL_TREE_DEPTH 0
 

diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <unistd.h>
 #endif
 
+#include <limits>
 #include <stack>
 
 #include <util/invariant.h>
@@ -28,7 +29,9 @@ Author: Daniel Kroening, [email protected]
 
 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
 {
-  dest.capacity(bv.size());
+  PRECONDITION(
+    bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
+  dest.capacity(static_cast<int>(bv.size()));
 
   forall_literals(it, bv)
     if(!it->is_false())