diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h index 1df94bdc9ce..cfb4d5a8286 100644 --- a/jbmc/src/java_bytecode/expr2java.h +++ b/jbmc/src/java_bytecode/expr2java.h @@ -58,7 +58,7 @@ std::string type2java(const typet &type, const namespacet &ns); template std::string floating_point_to_java_string(float_type value) { - const auto is_float = std::is_same::value; + static const bool is_float = std::is_same::value; static const std::string class_name = is_float ? "Float" : "Double"; if(std::isnan(value)) return class_name + ".NaN"; @@ -83,7 +83,7 @@ std::string floating_point_to_java_string(float_type value) { return std::stod(decimal) == value; } - catch(std::out_of_range) + catch(std::out_of_range &) { return false; } diff --git a/scripts/minisat-2.2.1-patch b/scripts/minisat-2.2.1-patch index d8129ec8e32..c4ef870bc99 100644 --- a/scripts/minisat-2.2.1-patch +++ b/scripts/minisat-2.2.1-patch @@ -227,3 +227,39 @@ index 9cbbc51..27b9700 100644 #include #endif +diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h +--- a/minisat/mtl/Vec.h ++++ b/minisat/mtl/Vec.h +@@ -96,8 +96,10 @@ + void vec::capacity(int min_cap) { + if (cap >= min_cap) return; + int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 +- if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) +- throw OutOfMemoryException(); ++ if (add > INT_MAX - cap) ++ throw OutOfMemoryException(); ++ ++ data = (T*)xrealloc(data, (cap += add) * sizeof(T)); + } + + +diff --git a/minisat/mtl/XAlloc.h b/minisat/mtl/XAlloc.h +--- a/minisat/mtl/XAlloc.h ++++ b/minisat/mtl/XAlloc.h +@@ -21,7 +21,6 @@ + #ifndef Minisat_XAlloc_h + #define Minisat_XAlloc_h + +-#include + #include + + namespace Minisat { +@@ -33,7 +32,7 @@ + static inline void* xrealloc(void *ptr, size_t size) + { + void* mem = realloc(ptr, size); +- if (mem == NULL && errno == ENOMEM){ ++ if (mem == NULL){ + throw OutOfMemoryException(); + }else + return mem; diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 3a54deac8f3..0ecfdef846f 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -33,23 +33,23 @@ hash_numbering value_set_fivrnst::function_numbering; static const char *alloc_adapter_prefix="alloc_adaptor::"; #define forall_objects(it, map) \ - for(object_map_dt::const_iterator (it) = (map).begin(); \ + for(object_map_dt::const_iterator it = (map).begin(); \ (it)!=(map).end(); \ (it)++) #define forall_valid_objects(it, map) \ - for(object_map_dt::const_iterator (it) = (map).begin(); \ + for(object_map_dt::const_iterator it = (map).begin(); \ (it)!=(map).end(); \ (it)++) \ if((map).is_valid_at((it)->first, from_function, from_target_index)) #define Forall_objects(it, map) \ - for(object_map_dt::iterator (it) = (map).begin(); \ + for(object_map_dt::iterator it = (map).begin(); \ (it)!=(map).end(); \ (it)++) #define Forall_valid_objects(it, map) \ - for(object_map_dt::iterator (it) = (map).begin(); \ + for(object_map_dt::iterator it = (map).begin(); \ (it)!=(map).end(); \ (it)++) \ if((map).is_valid_at((it)->first, from_function, from_target_index)) /* NOLINT(*) */