UnitTestBot · misonijnik · Jul 11, 2024 · Mar 21, 2024 · Mar 25, 2024 · Mar 25, 2024
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -17,6 +17,7 @@ env:
   ENABLE_DOXYGEN: 0
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
+  ENABLE_WARNINGS_AS_ERRORS: 1
   GTEST_VERSION: 1.11.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
   LLVM_VERSION: 11

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -678,10 +678,10 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
 ################################################################################
 # Set KLEE-specific include files
 ################################################################################
-include_directories("${CMAKE_BINARY_DIR}/include")
-include_directories("${CMAKE_SOURCE_DIR}/include")
-include_directories("${JSON_SRC_DIR}/include")
-include_directories("${IMMER_SRC_DIR}")
+include_directories(SYSTEM "${CMAKE_BINARY_DIR}/include")
+include_directories(SYSTEM "${CMAKE_SOURCE_DIR}/include")
+include_directories(SYSTEM "${JSON_SRC_DIR}/include")
+include_directories(SYSTEM "${IMMER_SRC_DIR}")
 # set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
 
 ################################################################################

diff --git a/Dockerfile b/Dockerfile
@@ -23,6 +23,7 @@ ENV ENABLE_DOXYGEN=1
 ENV ENABLE_OPTIMIZED=1
 ENV ENABLE_DEBUG=1
 ENV DISABLE_ASSERTIONS=0
+ENV ENABLE_WARNINGS_AS_ERRORS=0
 ENV REQUIRES_RTTI=0
 ENV SOLVERS=STP:Z3
 ENV GTEST_VERSION=1.11.0

diff --git a/build.sh b/build.sh
@@ -70,4 +70,6 @@ else
 fi
 done
 
-BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ./scripts/build/build.sh klee --install-system-deps
+ENABLE_WARNINGS_AS_ERRORS=0
+
+BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ./scripts/build/build.sh klee --install-system-deps
diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
@@ -10,17 +10,15 @@
 ###############################################################################
 # Compiler warnings
 ###############################################################################
-# FIXME: -Wunused-parameter fires a lot so for now suppress it.
 add_compile_options(
   "-Wall"
   "-Wextra"
-  "-Wno-unused-parameter"
 )
 
 ###############################################################################
 # Warnings as errors
 ###############################################################################
-option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
+option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" ON)
 if (WARNINGS_AS_ERRORS)
   add_compile_options("-Werror")
   message(STATUS "Treating compiler warnings as errors")

diff --git a/include/klee/ADT/Bits.h b/include/klee/ADT/Bits.h
@@ -10,14 +10,6 @@
 #ifndef KLEE_BITS_H
 #define KLEE_BITS_H
 
-#include "klee/Config/Version.h"
-
-#include "klee/Support/CompilerWarning.h"
-DISABLE_WARNING_PUSH
-DISABLE_WARNING_DEPRECATED_DECLARATIONS
-#include "llvm/Support/DataTypes.h"
-DISABLE_WARNING_POP
-
 #include <cassert>
 #include <cstddef>
 #include <cstdint>

diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h
@@ -2,19 +2,10 @@
 #define KLEE_DISJOINEDSETUNION_H
 
 #include "klee/ADT/Either.h"
-#include "klee/ADT/PersistentMap.h"
-#include "klee/ADT/PersistentSet.h"
 #include "klee/ADT/Ref.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/Symcrete.h"
 
-#include "klee/Support/CompilerWarning.h"
-DISABLE_WARNING_PUSH
-DISABLE_WARNING_DEPRECATED_DECLARATIONS
-#include "llvm/Support/raw_ostream.h"
-DISABLE_WARNING_POP
-
-#include <map>
 #include <set>
 #include <unordered_map>
 #include <unordered_set>

diff --git a/include/klee/ADT/FixedSizeStorageAdapter.h b/include/klee/ADT/FixedSizeStorageAdapter.h
@@ -1,6 +1,8 @@
 #ifndef KLEE_FIXEDSIZESTORAGEADAPTER_H
 #define KLEE_FIXEDSIZESTORAGEADAPTER_H
 
+#include "klee/Support/CompilerWarning.h"
+
 #ifndef IMMER_NO_EXCEPTIONS
 #define IMMER_NO_EXCEPTIONS
 #endif /* IMMER_NO_EXCEPTIONS */
@@ -109,6 +111,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
     ~iterator() {
@@ -127,6 +130,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
 
@@ -147,6 +151,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
       return *this;
     }
@@ -163,6 +168,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
     bool operator!=(const iterator &other) const {
@@ -178,6 +184,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
   };

diff --git a/include/klee/ADT/ImmutableTree.h b/include/klee/ADT/ImmutableTree.h
@@ -10,9 +10,9 @@
 #ifndef KLEE_IMMUTABLETREE_H
 #define KLEE_IMMUTABLETREE_H
 
+#include <algorithm>
 #include <cassert>
 #include <cstddef>
-#include <vector>
 
 namespace klee {
 template <class K, class V, class KOV, class CMP> class ImmutableTree {
@@ -259,8 +259,10 @@ ImmutableTree<K, V, KOV, CMP>::Node::~Node() {
 template <class K, class V, class KOV, class CMP>
 inline void ImmutableTree<K, V, KOV, CMP>::Node::decref() {
   --references;
-  if (references == 0)
+
+  if (references == 0 && !isTerminator()) {
     delete this;
+  }
 }
 
 template <class K, class V, class KOV, class CMP>

diff --git a/include/klee/ADT/Incremental.h b/include/klee/ADT/Incremental.h
@@ -272,7 +272,7 @@ class inc_uset {
       frame_index += framesSize();
     return frame_it(ids, frame_index);
   }
-  frame_it end(int frame_index) const { return frame_it(ids); }
+  frame_it end(int) const { return frame_it(ids); }
 
   void insert(const _Value &v) { ids[v].insert(current_frame); }
 

diff --git a/include/klee/ADT/StorageAdapter.h b/include/klee/ADT/StorageAdapter.h
@@ -2,6 +2,7 @@
 #define KLEE_STORAGEADAPTER_H
 
 #include "klee/ADT/PersistentHashMap.h"
+#include "klee/Support/CompilerWarning.h"
 
 #ifndef IMMER_NO_EXCEPTIONS
 #define IMMER_NO_EXCEPTIONS
@@ -139,6 +140,7 @@ struct StorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
     ~iterator() {
@@ -157,6 +159,7 @@ struct StorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
 
@@ -177,6 +180,7 @@ struct StorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
       return *this;
     }
@@ -193,6 +197,7 @@ struct StorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
     bool operator!=(const iterator &other) const {
@@ -208,6 +213,7 @@ struct StorageAdapter {
       }
       default:
         assert(0 && "unhandled iterator kind");
+        unreachable();
       }
     }
   };

diff --git a/include/klee/ADT/WeightedQueue.h b/include/klee/ADT/WeightedQueue.h
@@ -10,11 +10,12 @@
 #ifndef KLEE_WEIGHTEDQUEUE_H
 #define KLEE_WEIGHTEDQUEUE_H
 
-#include <deque>
 #include <functional>
 #include <map>
 #include <unordered_map>
 
+#include "klee/Support/CompilerWarning.h"
+
 namespace klee {
 
 template <class T, class Comparator = std::less<T>> class WeightedQueue {
@@ -109,7 +110,7 @@ T WeightedQueue<T, Comparator>::choose(
       return result;
     }
   }
-  assert(0 && "unreachable");
+  unreachable();
 }
 
 template <class T, class Comparator>

diff --git a/include/klee/Expr/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h
@@ -12,10 +12,7 @@
 #define KLEE_ARRAYEXPRHASH_H
 
 #include "klee/Expr/Expr.h"
-#include "klee/Solver/SolverStats.h"
-#include "klee/Statistics/TimerStatIncrementer.h"
 
-#include <map>
 #include <unordered_map>
 
 namespace klee {

diff --git a/include/klee/Expr/ArrayExprOptimizer.h b/include/klee/Expr/ArrayExprOptimizer.h
@@ -12,8 +12,6 @@
 
 #include <cstdint>
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
 #include <utility>
 #include <vector>
 

diff --git a/include/klee/Expr/ArrayExprRewriter.h b/include/klee/Expr/ArrayExprRewriter.h
@@ -10,7 +10,6 @@
 #ifndef KLEE_ARRAYEXPRREWRITER_H
 #define KLEE_ARRAYEXPRREWRITER_H
 
-#include <iterator>
 #include <map>
 #include <vector>
 

diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h
@@ -10,14 +10,10 @@
 #ifndef KLEE_ARRAYEXPRVISITOR_H
 #define KLEE_ARRAYEXPRVISITOR_H
 
-#include "klee/Expr/ExprBuilder.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprVisitor.h"
-#include "klee/Solver/SolverCmdLine.h"
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
 
 namespace klee {
 

diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
@@ -14,7 +14,6 @@
 #include "klee/ADT/SparseStorage.h"
 #include "klee/Expr/ExprEvaluator.h"
 
-#include <map>
 #include <set>
 
 namespace klee {

diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
@@ -21,7 +21,6 @@
 #include "klee/Expr/Path.h"
 #include "klee/Expr/Symcrete.h"
 
-#include <set>
 #include <vector>
 
 namespace klee {