Skip to content

Commit 24156e1

Browse files
S1eGamisonijnik
S1eGa
and
misonijnik
authored
Compile warnings fixes (#178)
* [refactor] Multiple fixes for compilation warnings. * [refactor] Added function. * [fix] Error handling in Z3. * [fix] Placed back bitwise AND in klee_prefer_cex. * [refactor] Included unistd in runtime, suppressed target overrides and reduntant include paths for runtime. Turned ON -Werror. * [refactor] Fixed CW for MetaSMT. * [chore] LLVM headers are made SYSTEM in cmake. * [chore] Update after rebase * [chore] Rebase on pointers-fixes. * [chore] Removed pragmas disabling warnings from system headers, removed reduntant includes. * [chore] Fixes. * [fix] Should JIT be included in External Dispatcher? MSan fails otherwise. * chore] Turned on -Wunused. --------- Co-authored-by: Aleksandr Misonizhnik <[email protected]>
1 parent 78f5095 commit 24156e1

File tree

210 files changed

+577
-1355
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

210 files changed

+577
-1355
lines changed

‎.github/workflows/build.yaml

+1
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ env:
1717
ENABLE_DOXYGEN: 0
1818
ENABLE_OPTIMIZED: 1
1919
ENABLE_DEBUG: 1
20+
ENABLE_WARNINGS_AS_ERRORS: 1
2021
GTEST_VERSION: 1.11.0
2122
KLEE_RUNTIME_BUILD: "Debug+Asserts"
2223
LLVM_VERSION: 11

‎CMakeLists.txt

+4-4
Original file line numberDiff line numberDiff line change
@@ -678,10 +678,10 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
678678
################################################################################
679679
# Set KLEE-specific include files
680680
################################################################################
681-
include_directories("${CMAKE_BINARY_DIR}/include")
682-
include_directories("${CMAKE_SOURCE_DIR}/include")
683-
include_directories("${JSON_SRC_DIR}/include")
684-
include_directories("${IMMER_SRC_DIR}")
681+
include_directories(SYSTEM "${CMAKE_BINARY_DIR}/include")
682+
include_directories(SYSTEM "${CMAKE_SOURCE_DIR}/include")
683+
include_directories(SYSTEM "${JSON_SRC_DIR}/include")
684+
include_directories(SYSTEM "${IMMER_SRC_DIR}")
685685
# set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
686686

687687
################################################################################

‎Dockerfile

+1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ ENV ENABLE_DOXYGEN=1
2323
ENV ENABLE_OPTIMIZED=1
2424
ENV ENABLE_DEBUG=1
2525
ENV DISABLE_ASSERTIONS=0
26+
ENV ENABLE_WARNINGS_AS_ERRORS=0
2627
ENV REQUIRES_RTTI=0
2728
ENV SOLVERS=STP:Z3
2829
ENV GTEST_VERSION=1.11.0

‎build.sh

+3-1
Original file line numberDiff line numberDiff line change
@@ -70,4 +70,6 @@ else
7070
fi
7171
done
7272

73-
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
73+
ENABLE_WARNINGS_AS_ERRORS=0
74+
75+
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

‎cmake/compiler_warnings.cmake

+1-3
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,15 @@
1010
###############################################################################
1111
# Compiler warnings
1212
###############################################################################
13-
# FIXME: -Wunused-parameter fires a lot so for now suppress it.
1413
add_compile_options(
1514
"-Wall"
1615
"-Wextra"
17-
"-Wno-unused-parameter"
1816
)
1917

2018
###############################################################################
2119
# Warnings as errors
2220
###############################################################################
23-
option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
21+
option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" ON)
2422
if (WARNINGS_AS_ERRORS)
2523
add_compile_options("-Werror")
2624
message(STATUS "Treating compiler warnings as errors")

‎include/klee/ADT/Bits.h

-8
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,6 @@
1010
#ifndef KLEE_BITS_H
1111
#define KLEE_BITS_H
1212

13-
#include "klee/Config/Version.h"
14-
15-
#include "klee/Support/CompilerWarning.h"
16-
DISABLE_WARNING_PUSH
17-
DISABLE_WARNING_DEPRECATED_DECLARATIONS
18-
#include "llvm/Support/DataTypes.h"
19-
DISABLE_WARNING_POP
20-
2113
#include <cassert>
2214
#include <cstddef>
2315
#include <cstdint>

‎include/klee/ADT/DisjointSetUnion.h

-9
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,10 @@
22
#define KLEE_DISJOINEDSETUNION_H
33

44
#include "klee/ADT/Either.h"
5-
#include "klee/ADT/PersistentMap.h"
6-
#include "klee/ADT/PersistentSet.h"
75
#include "klee/ADT/Ref.h"
86
#include "klee/Expr/Expr.h"
97
#include "klee/Expr/Symcrete.h"
108

11-
#include "klee/Support/CompilerWarning.h"
12-
DISABLE_WARNING_PUSH
13-
DISABLE_WARNING_DEPRECATED_DECLARATIONS
14-
#include "llvm/Support/raw_ostream.h"
15-
DISABLE_WARNING_POP
16-
17-
#include <map>
189
#include <set>
1910
#include <unordered_map>
2011
#include <unordered_set>

‎include/klee/ADT/FixedSizeStorageAdapter.h

+7
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#ifndef KLEE_FIXEDSIZESTORAGEADAPTER_H
22
#define KLEE_FIXEDSIZESTORAGEADAPTER_H
33

4+
#include "klee/Support/CompilerWarning.h"
5+
46
#ifndef IMMER_NO_EXCEPTIONS
57
#define IMMER_NO_EXCEPTIONS
68
#endif /* IMMER_NO_EXCEPTIONS */
@@ -109,6 +111,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
109111
}
110112
default:
111113
assert(0 && "unhandled iterator kind");
114+
unreachable();
112115
}
113116
}
114117
~iterator() {
@@ -127,6 +130,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
127130
}
128131
default:
129132
assert(0 && "unhandled iterator kind");
133+
unreachable();
130134
}
131135
}
132136

@@ -147,6 +151,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
147151
}
148152
default:
149153
assert(0 && "unhandled iterator kind");
154+
unreachable();
150155
}
151156
return *this;
152157
}
@@ -163,6 +168,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
163168
}
164169
default:
165170
assert(0 && "unhandled iterator kind");
171+
unreachable();
166172
}
167173
}
168174
bool operator!=(const iterator &other) const {
@@ -178,6 +184,7 @@ template <typename ValueType> struct FixedSizeStorageAdapter {
178184
}
179185
default:
180186
assert(0 && "unhandled iterator kind");
187+
unreachable();
181188
}
182189
}
183190
};

‎include/klee/ADT/ImmutableTree.h

+4-2
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,9 @@
1010
#ifndef KLEE_IMMUTABLETREE_H
1111
#define KLEE_IMMUTABLETREE_H
1212

13+
#include <algorithm>
1314
#include <cassert>
1415
#include <cstddef>
15-
#include <vector>
1616

1717
namespace klee {
1818
template <class K, class V, class KOV, class CMP> class ImmutableTree {
@@ -259,8 +259,10 @@ ImmutableTree<K, V, KOV, CMP>::Node::~Node() {
259259
template <class K, class V, class KOV, class CMP>
260260
inline void ImmutableTree<K, V, KOV, CMP>::Node::decref() {
261261
--references;
262-
if (references == 0)
262+
263+
if (references == 0 && !isTerminator()) {
263264
delete this;
265+
}
264266
}
265267

266268
template <class K, class V, class KOV, class CMP>

‎include/klee/ADT/Incremental.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,7 @@ class inc_uset {
272272
frame_index += framesSize();
273273
return frame_it(ids, frame_index);
274274
}
275-
frame_it end(int frame_index) const { return frame_it(ids); }
275+
frame_it end(int) const { return frame_it(ids); }
276276

277277
void insert(const _Value &v) { ids[v].insert(current_frame); }
278278

‎include/klee/ADT/StorageAdapter.h

+6
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
#define KLEE_STORAGEADAPTER_H
33

44
#include "klee/ADT/PersistentHashMap.h"
5+
#include "klee/Support/CompilerWarning.h"
56

67
#ifndef IMMER_NO_EXCEPTIONS
78
#define IMMER_NO_EXCEPTIONS
@@ -139,6 +140,7 @@ struct StorageAdapter {
139140
}
140141
default:
141142
assert(0 && "unhandled iterator kind");
143+
unreachable();
142144
}
143145
}
144146
~iterator() {
@@ -157,6 +159,7 @@ struct StorageAdapter {
157159
}
158160
default:
159161
assert(0 && "unhandled iterator kind");
162+
unreachable();
160163
}
161164
}
162165

@@ -177,6 +180,7 @@ struct StorageAdapter {
177180
}
178181
default:
179182
assert(0 && "unhandled iterator kind");
183+
unreachable();
180184
}
181185
return *this;
182186
}
@@ -193,6 +197,7 @@ struct StorageAdapter {
193197
}
194198
default:
195199
assert(0 && "unhandled iterator kind");
200+
unreachable();
196201
}
197202
}
198203
bool operator!=(const iterator &other) const {
@@ -208,6 +213,7 @@ struct StorageAdapter {
208213
}
209214
default:
210215
assert(0 && "unhandled iterator kind");
216+
unreachable();
211217
}
212218
}
213219
};

‎include/klee/ADT/WeightedQueue.h

+3-2
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,12 @@
1010
#ifndef KLEE_WEIGHTEDQUEUE_H
1111
#define KLEE_WEIGHTEDQUEUE_H
1212

13-
#include <deque>
1413
#include <functional>
1514
#include <map>
1615
#include <unordered_map>
1716

17+
#include "klee/Support/CompilerWarning.h"
18+
1819
namespace klee {
1920

2021
template <class T, class Comparator = std::less<T>> class WeightedQueue {
@@ -109,7 +110,7 @@ T WeightedQueue<T, Comparator>::choose(
109110
return result;
110111
}
111112
}
112-
assert(0 && "unreachable");
113+
unreachable();
113114
}
114115

115116
template <class T, class Comparator>

‎include/klee/Expr/ArrayExprHash.h

-3
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,7 @@
1212
#define KLEE_ARRAYEXPRHASH_H
1313

1414
#include "klee/Expr/Expr.h"
15-
#include "klee/Solver/SolverStats.h"
16-
#include "klee/Statistics/TimerStatIncrementer.h"
1715

18-
#include <map>
1916
#include <unordered_map>
2017

2118
namespace klee {

‎include/klee/Expr/ArrayExprOptimizer.h

-2
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@
1212

1313
#include <cstdint>
1414
#include <map>
15-
#include <unordered_map>
16-
#include <unordered_set>
1715
#include <utility>
1816
#include <vector>
1917

‎include/klee/Expr/ArrayExprRewriter.h

-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010
#ifndef KLEE_ARRAYEXPRREWRITER_H
1111
#define KLEE_ARRAYEXPRREWRITER_H
1212

13-
#include <iterator>
1413
#include <map>
1514
#include <vector>
1615

‎include/klee/Expr/ArrayExprVisitor.h

-4
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,10 @@
1010
#ifndef KLEE_ARRAYEXPRVISITOR_H
1111
#define KLEE_ARRAYEXPRVISITOR_H
1212

13-
#include "klee/Expr/ExprBuilder.h"
1413
#include "klee/Expr/ExprHashMap.h"
1514
#include "klee/Expr/ExprVisitor.h"
16-
#include "klee/Solver/SolverCmdLine.h"
1715

1816
#include <map>
19-
#include <unordered_map>
20-
#include <unordered_set>
2117

2218
namespace klee {
2319

‎include/klee/Expr/Assignment.h

-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
#include "klee/ADT/SparseStorage.h"
1515
#include "klee/Expr/ExprEvaluator.h"
1616

17-
#include <map>
1817
#include <set>
1918

2019
namespace klee {

‎include/klee/Expr/Constraints.h

-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@
2121
#include "klee/Expr/Path.h"
2222
#include "klee/Expr/Symcrete.h"
2323

24-
#include <set>
2524
#include <vector>
2625

2726
namespace klee {

0 commit comments

Comments
 (0)