From 4f3c102109c1a7fa1df551127e384990bd5098c7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 May 2018 13:30:25 +0100 Subject: [PATCH 1/4] Silence Minisat's use of realloc on non-POD and fix and use its xrealloc This was a new GCC 8 warning; testing on errno == ENOMEM with && opened the door for non-compliant implementations to fail to allocate without capacity() failing. --- scripts/minisat-2.2.1-patch | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) 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; From 0c00835c0ddb3920c9a5b1081c5b4c6cf3344c2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 May 2018 13:45:43 +0100 Subject: [PATCH 2/4] Do not use parentheses around the declared symbol GCC 8 doesn't like this. --- src/pointer-analysis/value_set_fivrns.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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(*) */ From 7211280656e1adebde7617a05c42372a1896a87e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 May 2018 13:47:00 +0100 Subject: [PATCH 3/4] Silence spurious GCC 8 warning For an unknown reason GCC 8 thinks is_float is never used. --- jbmc/src/java_bytecode/expr2java.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h index 1df94bdc9ce..7a960703ac2 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"; From e5f3c41f07a3028ada4bc4fbf422a97f1fe6494a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 May 2018 13:47:42 +0100 Subject: [PATCH 4/4] Use a reference with exception types that use vtables GCC 8 warns about this. --- jbmc/src/java_bytecode/expr2java.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h index 7a960703ac2..cfb4d5a8286 100644 --- a/jbmc/src/java_bytecode/expr2java.h +++ b/jbmc/src/java_bytecode/expr2java.h @@ -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; }