From 6c48e67e7a9eb3531b923121b56a12a7b089a0ae Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 20 Jul 2023 11:45:58 +0400 Subject: [PATCH] [fix] Update build.yaml and add come fixes --- .github/workflows/build.yaml | 15 ++++- CMakeLists.txt | 2 +- build.sh | 2 +- include/klee/ADT/Bits.h | 4 ++ include/klee/Expr/IndependentSet.h | 6 ++ include/klee/Expr/SymbolicSource.h | 4 ++ include/klee/Expr/Symcrete.h | 4 ++ include/klee/Module/InstructionInfoTable.h | 9 ++- include/klee/Module/KInstruction.h | 4 ++ include/klee/Module/KModule.h | 4 ++ include/klee/Module/KType.h | 2 +- include/klee/Module/Target.h | 6 +- include/klee/Support/Casting.h | 4 ++ include/klee/Support/CompilerWarning.h | 6 +- include/klee/Support/CompressionStream.h | 5 ++ include/klee/Support/Debug.h | 5 ++ include/klee/Support/PrintContext.h | 4 ++ include/klee/Support/RoundingModeUtil.h | 5 ++ include/klee/Support/Timer.h | 4 ++ include/klee/util/APFloatEval.h | 5 ++ lib/Core/CXXTypeSystem/CXXTypeManager.cpp | 9 ++- lib/Core/CXXTypeSystem/CXXTypeManager.h | 4 ++ lib/Core/Context.cpp | 5 ++ lib/Core/DistanceCalculator.cpp | 5 ++ lib/Core/ExecutionState.cpp | 4 ++ lib/Core/ExecutionState.h | 4 ++ lib/Core/Executor.cpp | 58 ++++++++++--------- lib/Core/Executor.h | 4 ++ lib/Core/Memory.cpp | 5 +- lib/Core/Memory.h | 6 +- lib/Core/MemoryManager.h | 1 - lib/Core/PTree.h | 5 ++ lib/Core/Searcher.h | 4 ++ lib/Core/TargetCalculator.h | 6 +- lib/Core/TypeManager.cpp | 4 ++ lib/Core/UserSearcher.cpp | 4 ++ lib/Core/UserSearcher.h | 4 ++ lib/Expr/APFloatEval.cpp | 6 ++ lib/Expr/ArrayExprOptimizer.cpp | 8 ++- lib/Expr/ArrayExprRewriter.cpp | 6 +- lib/Expr/AssignmentGenerator.cpp | 8 ++- lib/Expr/Constraints.cpp | 4 ++ lib/Expr/Expr.cpp | 4 ++ lib/Expr/ExprPPrinter.cpp | 5 ++ lib/Expr/ExprSMTLIBPrinter.cpp | 4 ++ lib/Expr/ExprVisitor.cpp | 4 ++ lib/Expr/Lexer.cpp | 4 ++ lib/Expr/Parser.cpp | 4 ++ lib/Expr/Path.cpp | 5 ++ lib/Expr/SymbolicSource.cpp | 3 + lib/Module/CallSplitter.cpp | 4 ++ lib/Module/CodeGraphDistance.cpp | 5 ++ lib/Module/FunctionAlias.cpp | 4 ++ .../InstructionOperandTypeCheckPass.cpp | 5 ++ lib/Module/KInstruction.cpp | 6 ++ lib/Module/KLEEIRMetaData.h | 4 ++ lib/Module/KType.cpp | 6 +- lib/Module/LowerSwitch.cpp | 1 + lib/Module/OptNone.cpp | 4 ++ lib/Module/ReturnSplitter.cpp | 4 ++ lib/Module/SarifReport.cpp | 4 ++ lib/Solver/CexCachingSolver.cpp | 4 ++ lib/Solver/ConcretizingSolver.cpp | 4 ++ lib/Solver/ConstructSolverChain.cpp | 4 ++ lib/Solver/CoreSolver.cpp | 9 ++- lib/Solver/FastCexSolver.cpp | 4 ++ lib/Solver/IndependentSolver.cpp | 7 ++- lib/Solver/MetaSMTBuilder.h | 5 ++ lib/Solver/MetaSMTSolver.cpp | 4 ++ lib/Solver/QueryLoggingSolver.h | 4 ++ lib/Solver/STPBuilder.cpp | 4 ++ lib/Solver/STPSolver.cpp | 4 ++ lib/Solver/SolverCmdLine.cpp | 4 ++ lib/Solver/Z3BitvectorBuilder.cpp | 5 ++ lib/Solver/Z3Builder.cpp | 4 ++ lib/Solver/Z3CoreBuilder.cpp | 4 ++ lib/Solver/Z3HashConfig.h | 7 ++- lib/Solver/Z3Solver.cpp | 8 ++- lib/Support/CompressionStream.cpp | 4 ++ lib/Support/FileHandling.cpp | 4 ++ lib/Support/PrintVersion.cpp | 8 ++- lib/Support/RoundingModeUtil.cpp | 6 ++ lib/Support/TreeStream.cpp | 5 ++ runtime/POSIX/fd_init.c | 2 +- runtime/Sanitizer/ubsan/ubsan_checks.inc | 5 +- scripts/.clang-format | 2 + test/Feature/const_array_opt1.c | 2 +- test/Feature/types/ArrayAccess.c | 2 +- test/Feature/types/InnerStructAccess.c | 2 +- test/Feature/types/StructDereference.c | 2 +- .../types/SymbolicPointerMultipleResolve.c | 2 +- .../types/SymbolicPointerSimpleResolve.c | 2 +- test/Feature/types/UnionAccess.c | 2 +- .../effective-type/EffectiveTypeFirstRead.c | 2 +- .../effective-type/EffectiveTypeMalloc.c | 2 +- .../effective-type/EffectiveTypeMemset.c | 2 +- .../effective-type/EffectiveTypeRealloc.c | 2 +- .../types/effective-type/OperatorNew.cpp | 2 +- .../ArrayPointerAlignment.c | 2 +- .../DefaultPointerAlignment.c | 2 +- .../EffectiveTypePointerAlignment.c | 2 +- .../StructurePointerAlignment.c | 2 +- .../StructurePointerWithOffsetAlignment.c | 2 +- test/Industry/if2.c | 2 +- test/Industry/while_true.c | 4 +- tools/kleaver/main.cpp | 4 ++ tools/ktest-gen/ktest-gen.cpp | 1 + tools/ktest-randgen/ktest-randgen.cpp | 4 +- unittests/Expr/ArrayExprTest.cpp | 6 +- unittests/Searcher/SearcherTest.cpp | 4 ++ unittests/Solver/SolverTest.cpp | 4 ++ unittests/TestMain.cpp | 4 ++ 112 files changed, 443 insertions(+), 89 deletions(-) create mode 100644 scripts/.clang-format diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index a89737d8fc..ef36613546 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -21,7 +21,6 @@ env: LLVM_VERSION: 11 MINISAT_VERSION: "master" REQUIRES_RTTI: 0 - SOLVERS: STP:Z3 STP_VERSION: 2.3.3 TCMALLOC_VERSION: 2.9.1 UCLIBC_VERSION: klee_uclibc_v1.3 @@ -56,22 +55,28 @@ jobs: - name: "LLVM 14" env: LLVM_VERSION: 14 + SOLVERS: Z3 - name: "LLVM 13" env: LLVM_VERSION: 13 + SOLVERS: Z3 - name: "LLVM 12" env: LLVM_VERSION: 12 + SOLVERS: Z3 - name: "LLVM 11, Doxygen" env: LLVM_VERSION: 11 ENABLE_DOXYGEN: 1 + SOLVERS: Z3 - name: "LLVM 10" env: LLVM_VERSION: 10 + SOLVERS: Z3 - name: "LLVM 9" env: LLVM_VERSION: 9 + SOLVERS: Z3 # Sanitizer builds. Do unoptimized build otherwise the optimizer # might remove problematic code - name: "ASan" @@ -79,12 +84,14 @@ jobs: SANITIZER_BUILD: address ENABLE_OPTIMIZED: 0 USE_TCMALLOC: 0 + SOLVERS: STP SANITIZER_LLVM_VERSION: 12 - name: "UBSan" env: SANITIZER_BUILD: undefined ENABLE_OPTIMIZED: 0 USE_TCMALLOC: 0 + SOLVERS: STP SANITIZER_LLVM_VERSION: 12 - name: "MSan" env: @@ -112,6 +119,7 @@ jobs: # Check we can build latest klee-uclibc branch - name: "Latest klee-uclibc" env: + SOLVERS: Z3 UCLIBC_VERSION: klee_0_9_29 # Check at least one build with Asserts disabled. - name: "Asserts disabled" @@ -121,6 +129,7 @@ jobs: # Check without TCMALLOC and with an optimised runtime library - name: "No TCMalloc, optimised runtime" env: + SOLVERS: STP USE_TCMALLOC: 0 KLEE_RUNTIME_BUILD: "Release+Debug+Asserts" steps: @@ -132,6 +141,7 @@ jobs: env: ${{ matrix.env }} run: scripts/build/build.sh klee --docker --create-final-image - name: Run tests + env: ${{ matrix.env }} run: scripts/build/run-tests.sh --run-docker --debug macOS: @@ -175,7 +185,7 @@ jobs: include: - name: "STP" env: - SOLVERS: STP:Z3 + SOLVERS: STP - name: "Z3" env: SOLVERS: Z3 @@ -195,6 +205,7 @@ jobs: env: ${{ matrix.env }} run: scripts/build/build.sh klee --docker --create-final-image - name: Run tests + env: ${{ matrix.env }} run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug clang-format: diff --git a/CMakeLists.txt b/CMakeLists.txt index 212b92099b..e8317d04c0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -17,7 +17,7 @@ project(KLEE CXX C) # Project version ############################################################################### set(KLEE_VERSION_MAJOR 3) -set(KLEE_VERSION_MINOR 0) +set(KLEE_VERSION_MINOR 0-utbot) set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}") # If a patch is needed, we can add KLEE_VERSION_PATCH diff --git a/build.sh b/build.sh index 3dcbc9c050..f57c2cd955 100755 --- a/build.sh +++ b/build.sh @@ -35,7 +35,7 @@ REQUIRES_RTTI=1 ## Solvers Required options # SOLVERS=STP -SOLVERS=Z3 +SOLVERS=STP:Z3 ## Google Test Required options GTEST_VERSION=1.11.0 diff --git a/include/klee/ADT/Bits.h b/include/klee/ADT/Bits.h index abad955e7e..20518fee10 100644 --- a/include/klee/ADT/Bits.h +++ b/include/klee/ADT/Bits.h @@ -12,7 +12,11 @@ #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 #include diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index 581f42ac04..9173d90678 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -4,7 +4,13 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Solver/Solver.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP + #include #include diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index 807dd59448..be65580f7b 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -3,9 +3,13 @@ #include "klee/ADT/Ref.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Argument.h" #include "llvm/IR/Instruction.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/Expr/Symcrete.h b/include/klee/Expr/Symcrete.h index c8ebab70c0..6646c4cf16 100644 --- a/include/klee/Expr/Symcrete.h +++ b/include/klee/Expr/Symcrete.h @@ -4,7 +4,11 @@ #include "klee/ADT/Ref.h" #include "klee/Expr/ExprUtil.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/Module/InstructionInfoTable.h b/include/klee/Module/InstructionInfoTable.h index 09575bf29b..c6a6902906 100644 --- a/include/klee/Module/InstructionInfoTable.h +++ b/include/klee/Module/InstructionInfoTable.h @@ -10,8 +10,13 @@ #ifndef KLEE_INSTRUCTIONINFOTABLE_H #define KLEE_INSTRUCTIONINFOTABLE_H -#include -#include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/ADT/Optional.h" +#include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP + #include #include #include diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h index f8ac81a9a9..865a752bfd 100644 --- a/include/klee/Module/KInstruction.h +++ b/include/klee/Module/KInstruction.h @@ -13,8 +13,12 @@ #include "klee/Config/Version.h" #include "klee/Module/InstructionInfoTable.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/DataTypes.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index e140b0ee6b..f7499f6c25 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -15,8 +15,12 @@ #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KCallable.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/ArrayRef.h" #include "llvm/IR/CFG.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/Module/KType.h b/include/klee/Module/KType.h index bfb549f9fa..59ab9021e2 100644 --- a/include/klee/Module/KType.h +++ b/include/klee/Module/KType.h @@ -18,7 +18,7 @@ class TypeManager; template class ref; -enum TypeSystemKind { LLVM, CXX }; +enum class TypeSystemKind { Default, Advanced }; class KType { friend TypeManager; diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index 984b8dee5e..b43726ab94 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -14,12 +14,16 @@ #include "klee/ADT/Ref.h" #include "klee/Module/KModule.h" #include "klee/Module/SarifReport.h" +#include "klee/Support/OptionCategories.h" #include "klee/System/Time.h" -#include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/Support/Casting.h b/include/klee/Support/Casting.h index 5b04380e74..d2cd1cb84e 100644 --- a/include/klee/Support/Casting.h +++ b/include/klee/Support/Casting.h @@ -12,7 +12,11 @@ #include "klee/Config/Version.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP namespace klee { diff --git a/include/klee/Support/CompilerWarning.h b/include/klee/Support/CompilerWarning.h index fae5d3dfe9..f3c6ccacfa 100644 --- a/include/klee/Support/CompilerWarning.h +++ b/include/klee/Support/CompilerWarning.h @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +// clang-format off #ifndef KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H #define KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H @@ -23,8 +24,8 @@ #if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0) #define DISABLE_WARNING_DEPRECATED_DECLARATIONS #else -#define DISABLE_WARNING_DEPRECATED_DECLARATIONS \ - DISABLE_WARNING(-Wdeprecated - declarations) +#define DISABLE_WARNING_DEPRECATED_DECLARATIONS + DISABLE_WARNING(-Wdeprecated-declarations) #endif #else @@ -37,3 +38,4 @@ #endif #endif // KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H +// clang-format off diff --git a/include/klee/Support/CompressionStream.h b/include/klee/Support/CompressionStream.h index 69578fa3f8..fe3d606d21 100644 --- a/include/klee/Support/CompressionStream.h +++ b/include/klee/Support/CompressionStream.h @@ -11,7 +11,12 @@ #define KLEE_COMPRESSIONSTREAM_H #include "zlib.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP namespace klee { const size_t BUFSIZE = 128 * 1024; diff --git a/include/klee/Support/Debug.h b/include/klee/Support/Debug.h index 13d45e22d0..594dc3f8a0 100644 --- a/include/klee/Support/Debug.h +++ b/include/klee/Support/Debug.h @@ -11,7 +11,12 @@ #define KLEE_DEBUG_H #include "klee/Config/config.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Debug.h" +DISABLE_WARNING_POP // We define wrappers around the LLVM DEBUG macros that are conditionalized on // whether the LLVM we are building against has the symbols needed by these diff --git a/include/klee/Support/PrintContext.h b/include/klee/Support/PrintContext.h index ab2df83401..e397367683 100644 --- a/include/klee/Support/PrintContext.h +++ b/include/klee/Support/PrintContext.h @@ -12,7 +12,11 @@ #include "klee/Expr/Expr.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/Support/RoundingModeUtil.h b/include/klee/Support/RoundingModeUtil.h index bf89a43cf7..562dabff19 100644 --- a/include/klee/Support/RoundingModeUtil.h +++ b/include/klee/Support/RoundingModeUtil.h @@ -7,7 +7,12 @@ // //===----------------------------------------------------------------------===// #ifndef KLEE_ROUNDING_MODE_UTIL_H + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/APFloat.h" +DISABLE_WARNING_POP namespace klee { diff --git a/include/klee/Support/Timer.h b/include/klee/Support/Timer.h index 4021f1560b..ea621ee2d3 100644 --- a/include/klee/Support/Timer.h +++ b/include/klee/Support/Timer.h @@ -12,7 +12,11 @@ #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/SmallVector.h" +DISABLE_WARNING_POP #include #include diff --git a/include/klee/util/APFloatEval.h b/include/klee/util/APFloatEval.h index 37f01a82b4..4f038aa40d 100644 --- a/include/klee/util/APFloatEval.h +++ b/include/klee/util/APFloatEval.h @@ -9,8 +9,13 @@ #ifndef KLEE_APFLOAT_EVAL_H #define KLEE_APFLOAT_EVAL_H + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/APFloat.h" #include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP namespace klee { diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp index 8e8952e00d..a171e65a9d 100644 --- a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp +++ b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp @@ -8,13 +8,16 @@ #include "klee/Module/KModule.h" #include "klee/Module/KType.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/DebugInfoMetadata.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Metadata.h" #include "llvm/IR/Module.h" #include "llvm/IR/Type.h" - #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP #include #include @@ -213,7 +216,7 @@ static ref getComplexPointerRestrictions( /* C++ KType base class */ cxxtypes::KCXXType::KCXXType(llvm::Type *type, TypeManager *parent) : KType(type, parent) { - typeSystemKind = TypeSystemKind::CXX; + typeSystemKind = TypeSystemKind::Advanced; typeKind = DEFAULT; } @@ -261,7 +264,7 @@ cxxtypes::CXXTypeKind cxxtypes::KCXXType::getTypeKind() const { } bool cxxtypes::KCXXType::classof(const KType *requestedType) { - return requestedType->getTypeSystemKind() == TypeSystemKind::CXX; + return requestedType->getTypeSystemKind() == TypeSystemKind::Advanced; } /* Composite type */ diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.h b/lib/Core/CXXTypeSystem/CXXTypeManager.h index cdc7f42360..3446091138 100644 --- a/lib/Core/CXXTypeSystem/CXXTypeManager.h +++ b/lib/Core/CXXTypeSystem/CXXTypeManager.h @@ -6,7 +6,11 @@ #include "klee/Expr/ExprHashMap.h" #include "klee/Module/KType.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp index d01b846e69..0ba40313d2 100644 --- a/lib/Core/Context.cpp +++ b/lib/Core/Context.cpp @@ -10,7 +10,12 @@ #include "klee/Core/Context.h" #include "klee/Expr/Expr.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Type.h" +DISABLE_WARNING_POP #include diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index 3010318085..08c8caf64e 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -12,8 +12,13 @@ #include "klee/Module/CodeGraphDistance.h" #include "klee/Module/KInstruction.h" #include "klee/Module/Target.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/CFG.h" #include "llvm/IR/IntrinsicInst.h" +DISABLE_WARNING_POP #include diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 76b6c70cba..9288283849 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -20,9 +20,13 @@ #include "klee/Support/Casting.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index dc671ce681..3e4c9d3c2a 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -26,7 +26,11 @@ #include "klee/Solver/Solver.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3b661e1a38..b7b0bc49bc 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -69,6 +69,9 @@ #include "klee/System/MemoryUsage.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Attributes.h" @@ -94,6 +97,7 @@ typedef unsigned TypeSize; #endif #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include @@ -137,26 +141,22 @@ cl::OptionCategory TestGenCat("Test generation options", cl::OptionCategory LazyInitCat("Lazy initialization option", "These options configure lazy initialization."); -cl::opt - TypeSystem("type-system", - cl::desc("Use information about type system from specified " - "language (default=llvm)"), - cl::values(clEnumValN(TypeSystemKind::LLVM, "LLVM", - "Use plain type system from LLVM"), - clEnumValN(TypeSystemKind::CXX, "CXX", - "Use type system from CXX")), - cl::init(TypeSystemKind::LLVM), cl::cat(ExecCat)); +cl::opt UseAdvancedTypeSystem( + "use-advanced-type-system", + cl::desc("Use advanced information about type system from " + "language (default=false)"), + cl::init(false), cl::cat(ExecCat)); cl::opt MergedPointerDereference( "use-merged-pointer-dereference", cl::init(false), cl::desc("Enable merged pointer dereference (default=false)"), cl::cat(ExecCat)); -cl::opt - UseTBAA("use-tbaa", - cl::desc("Turns on restrictions based on types compatibility for " - "symbolic pointers (default=false)"), - cl::init(false), cl::cat(ExecCat)); +cl::opt UseTypeBasedAliasAnalysis( + "use-tbaa", + cl::desc("Turns on restrictions based on types compatibility for " + "symbolic pointers (default=false)"), + cl::init(false), cl::cat(ExecCat)); cl::opt AlignSymbolicPointers("align-symbolic-pointers", @@ -4195,10 +4195,21 @@ void Executor::reportProgressTowardsTargets(std::string prefix, for (auto &p : distancesTowardsTargets) { auto target = p.first; auto distance = p.second; - klee_message("%s for %s (lines %d to %d)", distance.toString().c_str(), - target->toString().c_str(), - target->getBlock()->getFirstInstruction()->info->line, - target->getBlock()->getLastInstruction()->info->line); + std::ostringstream repr; + repr << "Target " << target->getId() << ": "; + if (target->shouldFailOnThisTarget()) { + repr << "error "; + } + repr << "in function " + + target->getBlock()->parent->function->getName().str(); + repr << " (lines "; + repr << target->getBlock()->getFirstInstruction()->info->line; + repr << " to "; + repr << target->getBlock()->getLastInstruction()->info->line; + repr << ")"; + std::string targetString = repr.str(); + klee_message("%s for %s", distance.toString().c_str(), + targetString.c_str()); } } @@ -4292,15 +4303,10 @@ void Executor::runWithTarget(ExecutionState &state, KFunction *kf, } void Executor::initializeTypeManager() { - switch (TypeSystem) { - case (TypeSystemKind::LLVM): - typeSystemManager = new TypeManager(kmodule.get()); - break; - case (TypeSystemKind::CXX): + if (UseAdvancedTypeSystem) { typeSystemManager = new CXXTypeManager(kmodule.get()); - break; - default: - assert(false && "Unknown type system!"); + } else { + typeSystemManager = new TypeManager(kmodule.get()); } typeSystemManager->initModule(); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 9d037ae8d6..582c22f0f0 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -34,10 +34,14 @@ #include "klee/Solver/ConcretizationManager.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/Twine.h" #include "llvm/IR/Argument.h" #include "llvm/IR/Intrinsics.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index c2106afc5d..f85ea95b3b 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -28,12 +28,12 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/Value.h" +#include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" DISABLE_WARNING_POP #include -#include #include using namespace llvm; @@ -663,5 +663,6 @@ void ObjectState::print() const { KType *ObjectState::getDynamicType() const { return dynamicType; } bool ObjectState::isAccessableFrom(KType *accessingType) const { - return !UseTBAA || dynamicType->isAccessableFrom(accessingType); + return !UseTypeBasedAliasAnalysis || + dynamicType->isAccessableFrom(accessingType); } diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 0bd3be12f4..e43e4d015b 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -18,7 +18,11 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/SourceBuilder.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" +DISABLE_WARNING_POP #include #include @@ -39,7 +43,7 @@ class Solver; typedef uint64_t IDType; -extern llvm::cl::opt UseTBAA; +extern llvm::cl::opt UseTypeBasedAliasAnalysis; class MemoryObject { friend class STPBuilder; diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h index 12945d7b68..bc31477e2f 100644 --- a/lib/Core/MemoryManager.h +++ b/lib/Core/MemoryManager.h @@ -12,7 +12,6 @@ #include "klee/Expr/Expr.h" -#include "klee/Expr/SourceBuilder.h" #include #include #include diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 02602a247c..b0f3e0f320 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -13,7 +13,12 @@ #include "klee/Core/BranchTypes.h" #include "klee/Expr/Expr.h" #include "klee/Support/ErrorHandling.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/PointerIntPair.h" +DISABLE_WARNING_POP namespace klee { class ExecutionState; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 3467f59339..0469a00724 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -18,8 +18,12 @@ #include "klee/Module/KModule.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index b63f3673c8..3b99fb1913 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -14,12 +14,16 @@ #include "klee/Module/KModule.h" #include "klee/Module/Target.h" #include "klee/Module/TargetHash.h" +#include "klee/Support/OptionCategories.h" #include "klee/System/Time.h" -#include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/TypeManager.cpp b/lib/Core/TypeManager.cpp index 83d4ec8867..c6e00f2f82 100644 --- a/lib/Core/TypeManager.cpp +++ b/lib/Core/TypeManager.cpp @@ -7,11 +7,15 @@ #include "klee/Module/KModule.h" #include "klee/Module/KType.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/Module.h" #include "llvm/IR/Type.h" #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 72800087b9..ab86548677 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -16,7 +16,11 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP using namespace llvm; using namespace klee; diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h index 657a2d755c..d11ab791e5 100644 --- a/lib/Core/UserSearcher.h +++ b/lib/Core/UserSearcher.h @@ -10,7 +10,11 @@ #ifndef KLEE_USERSEARCHER_H #define KLEE_USERSEARCHER_H +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP namespace klee { class Executor; diff --git a/lib/Expr/APFloatEval.cpp b/lib/Expr/APFloatEval.cpp index f995d9ab78..a1f49b28f9 100644 --- a/lib/Expr/APFloatEval.cpp +++ b/lib/Expr/APFloatEval.cpp @@ -8,7 +8,13 @@ //===----------------------------------------------------------------------===// #include "klee/util/APFloatEval.h" #include "klee/Config/Version.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP + #include #include #include diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 3781b26365..d67bd3ddbd 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -20,8 +20,12 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" -#include -#include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/ADT/APInt.h" +#include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp index ab2f13b878..68eabf8260 100644 --- a/lib/Expr/ArrayExprRewriter.cpp +++ b/lib/Expr/ArrayExprRewriter.cpp @@ -13,7 +13,11 @@ #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Support/Casting.h" -#include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/ADT/APInt.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index 9110b67932..601ceb66e6 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -14,8 +14,12 @@ #include "klee/Support/ErrorHandling.h" #include "klee/klee.h" -#include -#include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/ADT/APInt.h" +#include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index a52db8dd2d..802a75bea4 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -20,8 +20,12 @@ #include "klee/Module/KModule.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP #include diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index a1bfcb658e..5df6320731 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -18,6 +18,9 @@ #include "klee/Support/RoundingModeUtil.h" #include "klee/util/APFloatEval.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/Hashing.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(13, 0) @@ -25,6 +28,7 @@ #endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 0585a8dbaa..bde8d30d6d 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -15,8 +15,13 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Support/PrintContext.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 448937aa69..e1a9b9aa89 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -11,8 +11,12 @@ #include "klee/Support/Casting.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index 6d2e509f33..e33219d20f 100644 --- a/lib/Expr/ExprVisitor.cpp +++ b/lib/Expr/ExprVisitor.cpp @@ -11,7 +11,11 @@ #include "klee/Expr/Expr.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP namespace { llvm::cl::opt UseVisitorHash( diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index 26eed1b172..9be58ae5ce 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -9,8 +9,12 @@ #include "klee/Expr/Parser/Lexer.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 98af5920ef..b072cec826 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -21,9 +21,13 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/APInt.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/Path.cpp b/lib/Expr/Path.cpp index 90861f3f3e..7b578aa30c 100644 --- a/lib/Expr/Path.cpp +++ b/lib/Expr/Path.cpp @@ -2,8 +2,13 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP using namespace klee; using namespace llvm; diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index ecb5ee6386..0e7f8b1086 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -6,8 +6,11 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/BasicBlock.h" #include "llvm/IR/Function.h" +DISABLE_WARNING_POP #include diff --git a/lib/Module/CallSplitter.cpp b/lib/Module/CallSplitter.cpp index d8b6931116..4c4a71c4f3 100644 --- a/lib/Module/CallSplitter.cpp +++ b/lib/Module/CallSplitter.cpp @@ -10,10 +10,14 @@ #include "Passes.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/Module.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" +DISABLE_WARNING_POP using namespace llvm; diff --git a/lib/Module/CodeGraphDistance.cpp b/lib/Module/CodeGraphDistance.cpp index 9fb483355b..5bcae51d26 100644 --- a/lib/Module/CodeGraphDistance.cpp +++ b/lib/Module/CodeGraphDistance.cpp @@ -9,7 +9,12 @@ //===----------------------------------------------------------------------===// #include "klee/Module/CodeGraphDistance.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/CFG.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Module/FunctionAlias.cpp b/lib/Module/FunctionAlias.cpp index aa80b35d6e..04afffff5d 100644 --- a/lib/Module/FunctionAlias.cpp +++ b/lib/Module/FunctionAlias.cpp @@ -13,9 +13,13 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/GlobalAlias.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Regex.h" +DISABLE_WARNING_POP using namespace llvm; diff --git a/lib/Module/InstructionOperandTypeCheckPass.cpp b/lib/Module/InstructionOperandTypeCheckPass.cpp index 650f44f348..3c836afc32 100644 --- a/lib/Module/InstructionOperandTypeCheckPass.cpp +++ b/lib/Module/InstructionOperandTypeCheckPass.cpp @@ -9,7 +9,12 @@ #include "Passes.h" #include "klee/Config/Version.h" #include "klee/Support/ErrorHandling.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP using namespace llvm; diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp index 2475cb29d8..f7159c4bd6 100644 --- a/lib/Module/KInstruction.cpp +++ b/lib/Module/KInstruction.cpp @@ -9,7 +9,13 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" +DISABLE_WARNING_POP + #include using namespace llvm; diff --git a/lib/Module/KLEEIRMetaData.h b/lib/Module/KLEEIRMetaData.h index 235ede74a6..edf6a45bee 100644 --- a/lib/Module/KLEEIRMetaData.h +++ b/lib/Module/KLEEIRMetaData.h @@ -10,7 +10,11 @@ #ifndef KLEE_KLEEIRMETADATA_H #define KLEE_KLEEIRMETADATA_H +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/MDBuilder.h" +DISABLE_WARNING_POP namespace klee { diff --git a/lib/Module/KType.cpp b/lib/Module/KType.cpp index 0111928caf..dea8be27ca 100644 --- a/lib/Module/KType.cpp +++ b/lib/Module/KType.cpp @@ -4,18 +4,22 @@ #include "klee/Expr/Expr.h" #include "klee/Module/KModule.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/DataLayout.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Type.h" #include "llvm/Support/Casting.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP using namespace klee; using namespace llvm; KType::KType(llvm::Type *type, TypeManager *parent) : type(type), parent(parent) { - typeSystemKind = TypeSystemKind::LLVM; + typeSystemKind = TypeSystemKind::Default; /* Type itself can be reached at offset 0 */ innerTypes[this].insert(0); } diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp index 474b9bf9a1..2f614f1d8c 100644 --- a/lib/Module/LowerSwitch.cpp +++ b/lib/Module/LowerSwitch.cpp @@ -16,6 +16,7 @@ #include "Passes.h" #include "klee/Config/Version.h" + #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS diff --git a/lib/Module/OptNone.cpp b/lib/Module/OptNone.cpp index 255ab9ebd7..6e57090103 100644 --- a/lib/Module/OptNone.cpp +++ b/lib/Module/OptNone.cpp @@ -11,10 +11,14 @@ #include "klee/Config/Version.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/SmallPtrSet.h" #include "llvm/IR/Function.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/Module.h" +DISABLE_WARNING_POP namespace klee { diff --git a/lib/Module/ReturnSplitter.cpp b/lib/Module/ReturnSplitter.cpp index c88ebbbdfc..56ed05b8f0 100644 --- a/lib/Module/ReturnSplitter.cpp +++ b/lib/Module/ReturnSplitter.cpp @@ -10,10 +10,14 @@ #include "Passes.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/IR/Instruction.h" #include "llvm/IR/Module.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" +DISABLE_WARNING_POP using namespace llvm; diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp index 1641b52f93..a78292d33b 100644 --- a/lib/Module/SarifReport.cpp +++ b/lib/Module/SarifReport.cpp @@ -13,7 +13,11 @@ #include "klee/Module/KModule.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/IntrinsicInst.h" +DISABLE_WARNING_POP using namespace llvm; using namespace klee; diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index b03d377efa..da3303359d 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -19,7 +19,11 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index ba25dd990d..6fbbce8855 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -13,7 +13,11 @@ #include "klee/Solver/SolverImpl.h" #include "klee/Solver/SolverUtil.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Casting.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 7dd82625a6..6877337983 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -17,7 +17,11 @@ #include "klee/Support/ErrorHandling.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index d07aa32d7a..b6de1024b8 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -15,8 +15,12 @@ #include "klee/Solver/SolverCmdLine.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include @@ -28,11 +32,6 @@ std::unique_ptr createCoreSolver(CoreSolverType cst) { case STP_SOLVER: #ifdef ENABLE_STP klee_message("Using STP solver backend"); - if (ProduceUnsatCore) { - ProduceUnsatCore = false; - klee_message( - "Unsat cores are only supported by Z3, disabling unsat cores."); - } return std::make_unique(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 6e746deeab..3ba7904ac4 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -19,8 +19,12 @@ #include "klee/Support/Debug.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/APInt.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 06d9099b30..9e0139200a 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -9,7 +9,7 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Solver/SolverUtil.h" -#include "llvm/Support/Casting.h" + #define DEBUG_TYPE "independent-solver" #include "klee/Solver/Solver.h" @@ -22,7 +22,12 @@ #include "klee/Solver/SolverImpl.h" #include "klee/Support/Debug.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/Casting.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 59701e263f..b2418b8f91 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -20,8 +20,13 @@ #ifdef ENABLE_METASMT +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" +#include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 92694f8320..17e0972904 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -19,7 +19,11 @@ #include "klee/Solver/SolverImpl.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP #include diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index a9ca5000f3..16e50f5546 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -15,7 +15,11 @@ #include "klee/Solver/SolverImpl.h" #include "klee/System/Time.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 22897dd7fd..3ee8fbe2b7 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -17,9 +17,13 @@ #include "ConstantDivision.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP #include diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 14dac67fa6..4893115926 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -20,8 +20,12 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 8cbc5157ea..a4329a80b3 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -17,9 +17,13 @@ #include "klee/Config/Version.h" #include "klee/Support/OptionCategories.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/StringMap.h" #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP using namespace llvm; diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp index 9bb698f3c3..f673949618 100644 --- a/lib/Solver/Z3BitvectorBuilder.cpp +++ b/lib/Solver/Z3BitvectorBuilder.cpp @@ -18,8 +18,13 @@ #include "klee/Solver/Solver.h" #include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP using namespace klee; diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 59b88765e5..39cdf1918d 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -17,9 +17,13 @@ #include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/ADT/iterator_range.h" #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP using namespace klee; diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp index e2d17a7128..687c0e47db 100644 --- a/lib/Solver/Z3CoreBuilder.cpp +++ b/lib/Solver/Z3CoreBuilder.cpp @@ -17,7 +17,11 @@ #include "klee/Expr/Expr.h" #include "klee/Solver/SolverStats.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP using namespace klee; diff --git a/lib/Solver/Z3HashConfig.h b/lib/Solver/Z3HashConfig.h index 82d091ad23..87c8d347ec 100644 --- a/lib/Solver/Z3HashConfig.h +++ b/lib/Solver/Z3HashConfig.h @@ -10,8 +10,13 @@ #ifndef KLEE_Z3HASHCONFIG_H #define KLEE_Z3HASHCONFIG_H +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP + #include -#include namespace Z3HashConfig { extern llvm::cl::opt UseConstructHashZ3; diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 1bedf90cbc..cfcb5d6b57 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -59,7 +59,11 @@ llvm::cl::opt llvm::cl::cat(klee::SolvingCat)); } // namespace +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP namespace klee { @@ -146,9 +150,7 @@ Z3SolverImpl::Z3SolverImpl(Z3BuilderType type) Z3_params_inc_ref(builder->ctx, solverParameters); timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout"); setCoreSolverTimeout(timeout); - if (ProduceUnsatCore) { - unsatCoreParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "unsat_core"); - } + unsatCoreParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "unsat_core"); // HACK: This changes Z3's handling of the `to_ieee_bv` function so that // we get a signal bit pattern interpretation for NaN. At the time of writing diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp index 005f6e3b66..1b81048738 100644 --- a/lib/Support/CompressionStream.cpp +++ b/lib/Support/CompressionStream.cpp @@ -11,7 +11,11 @@ #ifdef HAVE_ZLIB_H #include "klee/Support/CompressionStream.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/FileSystem.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Support/FileHandling.cpp b/lib/Support/FileHandling.cpp index dc86ce4119..17a2fc0697 100644 --- a/lib/Support/FileHandling.cpp +++ b/lib/Support/FileHandling.cpp @@ -12,7 +12,11 @@ #include "klee/Config/config.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/FileSystem.h" +DISABLE_WARNING_POP #ifdef HAVE_ZLIB_H #include "klee/Support/CompressionStream.h" diff --git a/lib/Support/PrintVersion.cpp b/lib/Support/PrintVersion.cpp index 0a72f70f25..ad799f9dfb 100644 --- a/lib/Support/PrintVersion.cpp +++ b/lib/Support/PrintVersion.cpp @@ -8,12 +8,16 @@ //===----------------------------------------------------------------------===// #include "klee/Support/PrintVersion.h" +#include "klee/Config/CompileTimeInfo.h" #include "klee/Config/Version.h" #include "klee/Config/config.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" - -#include "klee/Config/CompileTimeInfo.h" +DISABLE_WARNING_POP void klee::printVersion(llvm::raw_ostream &OS) { OS << PACKAGE_STRING " (" PACKAGE_URL ")\n"; diff --git a/lib/Support/RoundingModeUtil.cpp b/lib/Support/RoundingModeUtil.cpp index 334bcdf709..d8b8d0d81a 100644 --- a/lib/Support/RoundingModeUtil.cpp +++ b/lib/Support/RoundingModeUtil.cpp @@ -7,7 +7,13 @@ // //===----------------------------------------------------------------------===// #include "klee/Support/RoundingModeUtil.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP + #include namespace klee { diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index a4a8e17b63..55c85de174 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -18,7 +18,12 @@ #include #include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP + #include using namespace klee; diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 4989022505..02469b8696 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -168,7 +168,7 @@ void klee_init_fds(unsigned n_files, unsigned file_length, __exe_env.fds[0].dfile = __exe_fs.sym_stdin; off64_t *ptr = malloc(sizeof(off64_t)); klee_make_symbolic(ptr, sizeof(off64_t), "stdin_read"); - mempcpy(&__exe_env.stdin_off, ptr, sizeof(off64_t)); + memcpy(&__exe_env.stdin_off, ptr, sizeof(off64_t)); free(ptr); __exe_env.max_off = 0; } else diff --git a/runtime/Sanitizer/ubsan/ubsan_checks.inc b/runtime/Sanitizer/ubsan/ubsan_checks.inc index 35c64f41ff..964dfc99b1 100644 --- a/runtime/Sanitizer/ubsan/ubsan_checks.inc +++ b/runtime/Sanitizer/ubsan/ubsan_checks.inc @@ -18,7 +18,7 @@ #include "klee/Config/Version.h" #ifndef UBSAN_CHECK -# error "Define UBSAN_CHECK prior to including this file!" +#error "Define UBSAN_CHECK prior to including this file!" #endif // UBSAN_CHECK(Name, SummaryKind, FSanitizeFlagName) @@ -58,8 +58,7 @@ UBSAN_CHECK(ImplicitUnsignedIntegerTruncation, UBSAN_CHECK(ImplicitSignedIntegerTruncation, "implicit-signed-integer-truncation", "implicit-signed-integer-truncation") -UBSAN_CHECK(ImplicitIntegerSignChange, - "implicit-integer-sign-change", +UBSAN_CHECK(ImplicitIntegerSignChange, "implicit-integer-sign-change", "implicit-integer-sign-change") UBSAN_CHECK(ImplicitSignedIntegerTruncationOrSignChange, "implicit-signed-integer-truncation-or-sign-change", diff --git a/scripts/.clang-format b/scripts/.clang-format new file mode 100644 index 0000000000..a43d914ec3 --- /dev/null +++ b/scripts/.clang-format @@ -0,0 +1,2 @@ +DisableFormat: true +SortIncludes: false \ No newline at end of file diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c index 0a2ebd8811..7482d48232 100644 --- a/test/Feature/const_array_opt1.c +++ b/test/Feature/const_array_opt1.c @@ -3,7 +3,7 @@ // Disabling msan and ubsan because it times out on CI // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --const-array-opt --use-guided-search=none --max-time=10 --only-output-states-covering-new %t.bc | FileCheck %s /* This is testing the const array optimization. On my 2.3GHz machine this takes under 2 seconds w/ the optimization and almost 6 minutes diff --git a/test/Feature/types/ArrayAccess.c b/test/Feature/types/ArrayAccess.c index 523449d2c5..3fa710303c 100644 --- a/test/Feature/types/ArrayAccess.c +++ b/test/Feature/types/ArrayAccess.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/InnerStructAccess.c b/test/Feature/types/InnerStructAccess.c index 55b08fe89c..6062430983 100644 --- a/test/Feature/types/InnerStructAccess.c +++ b/test/Feature/types/InnerStructAccess.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/StructDereference.c b/test/Feature/types/StructDereference.c index 114a31bb0b..a42bcb37ec 100644 --- a/test/Feature/types/StructDereference.c +++ b/test/Feature/types/StructDereference.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/SymbolicPointerMultipleResolve.c b/test/Feature/types/SymbolicPointerMultipleResolve.c index 94c0cf77c1..bf8e73217f 100644 --- a/test/Feature/types/SymbolicPointerMultipleResolve.c +++ b/test/Feature/types/SymbolicPointerMultipleResolve.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/SymbolicPointerSimpleResolve.c b/test/Feature/types/SymbolicPointerSimpleResolve.c index c8f2d272c2..957ba1c2d1 100644 --- a/test/Feature/types/SymbolicPointerSimpleResolve.c +++ b/test/Feature/types/SymbolicPointerSimpleResolve.c @@ -4,7 +4,7 @@ // RUN: echo "x" >> %t.res // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --skip-local=false --use-gep-opt %t.bc >%t.log +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --skip-local=false --use-gep-opt %t.bc >%t.log // RUN: diff %t.res %t.log #include "klee/klee.h" diff --git a/test/Feature/types/UnionAccess.c b/test/Feature/types/UnionAccess.c index a1eddebe0c..013a0bfb29 100644 --- a/test/Feature/types/UnionAccess.c +++ b/test/Feature/types/UnionAccess.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/effective-type/EffectiveTypeFirstRead.c b/test/Feature/types/effective-type/EffectiveTypeFirstRead.c index 7742ccc475..8b6d359f67 100644 --- a/test/Feature/types/effective-type/EffectiveTypeFirstRead.c +++ b/test/Feature/types/effective-type/EffectiveTypeFirstRead.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/effective-type/EffectiveTypeMalloc.c b/test/Feature/types/effective-type/EffectiveTypeMalloc.c index 8ae9d2eb2d..a5c32d7efc 100644 --- a/test/Feature/types/effective-type/EffectiveTypeMalloc.c +++ b/test/Feature/types/effective-type/EffectiveTypeMalloc.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/effective-type/EffectiveTypeMemset.c b/test/Feature/types/effective-type/EffectiveTypeMemset.c index d85ff23cf1..6301b21e29 100644 --- a/test/Feature/types/effective-type/EffectiveTypeMemset.c +++ b/test/Feature/types/effective-type/EffectiveTypeMemset.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" diff --git a/test/Feature/types/effective-type/EffectiveTypeRealloc.c b/test/Feature/types/effective-type/EffectiveTypeRealloc.c index 85ab878d73..cf8501f08b 100644 --- a/test/Feature/types/effective-type/EffectiveTypeRealloc.c +++ b/test/Feature/types/effective-type/EffectiveTypeRealloc.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/effective-type/OperatorNew.cpp b/test/Feature/types/effective-type/OperatorNew.cpp index 6cbd452a8e..dde3bb0478 100644 --- a/test/Feature/types/effective-type/OperatorNew.cpp +++ b/test/Feature/types/effective-type/OperatorNew.cpp @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c b/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c index 2b17b4b401..040eaec176 100644 --- a/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c +++ b/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c index 8a2f1fe5c8..3a21e7e1ea 100644 --- a/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c +++ b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --type-system=CXX --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --skip-local=false --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --skip-local=false --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c b/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c index a88b36ae43..ba52fd624c 100644 --- a/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c +++ b/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --use-advanced-type-system --use-tbaa --use-lazy-initialization=none --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/pointers-alignment/StructurePointerAlignment.c b/test/Feature/types/pointers-alignment/StructurePointerAlignment.c index b419ecfe2e..452ffebfdc 100644 --- a/test/Feature/types/pointers-alignment/StructurePointerAlignment.c +++ b/test/Feature/types/pointers-alignment/StructurePointerAlignment.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --type-system=CXX --use-tbaa --use-lazy-initialization=all --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --use-advanced-type-system --use-tbaa --use-lazy-initialization=all --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c b/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c index 57d255d7c8..9fffde0325 100644 --- a/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c +++ b/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --type-system=CXX --use-tbaa --use-lazy-initialization=all --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --ubsan-runtime --use-advanced-type-system --use-tbaa --use-lazy-initialization=all --align-symbolic-pointers=true --use-gep-opt %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Industry/if2.c b/test/Industry/if2.c index 3e4990abbe..38eabcc472 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -15,4 +15,4 @@ int main(int x) { // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE -// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in %13 in function main (lines 8 to 8) +// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in function main (lines 8 to 8) diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c index 0126452f02..4a75fdfd86 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -15,11 +15,11 @@ int main() { // RUN: FileCheck -input-file=%t.klee-out-1/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 0.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-1/messages.txt %s -check-prefix=CHECK-REACH-1 -// CHECK-REACH-1: (0, 1, 4) for Target 1: error in %while.end in function main (lines 8 to 8) +// CHECK-REACH-1: (0, 1, 4) for Target 1: error in function main (lines 8 to 8) // RUN: rm -rf %t.klee-out-2 // RUN: %klee --output-dir=%t.klee-out-2 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=50000 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out-2/warnings.txt %s -check-prefix=CHECK-ALL // CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-2/messages.txt %s -check-prefix=CHECK-REACH-2 -// CHECK-REACH-2: (0, 1, 1) for Target 1: error in %while.end in function main (lines 8 to 8) +// CHECK-REACH-2: (0, 1, 1) for Target 1: error in function main (lines 8 to 8) diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 623aab97c8..5d20590afe 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -26,12 +26,16 @@ #include "klee/Support/OptionCategories.h" #include "klee/Support/PrintVersion.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ManagedStatic.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/Signals.h" #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP #include #include diff --git a/tools/ktest-gen/ktest-gen.cpp b/tools/ktest-gen/ktest-gen.cpp index a15e847ff5..cfa01bacd1 100644 --- a/tools/ktest-gen/ktest-gen.cpp +++ b/tools/ktest-gen/ktest-gen.cpp @@ -20,6 +20,7 @@ #if defined(__FreeBSD__) || defined(__minix) || defined(__APPLE__) #define stat64 stat +#define off64_t off_t #endif #define MAX 64 diff --git a/tools/ktest-randgen/ktest-randgen.cpp b/tools/ktest-randgen/ktest-randgen.cpp index 682e24117c..1b94c820e7 100644 --- a/tools/ktest-randgen/ktest-randgen.cpp +++ b/tools/ktest-randgen/ktest-randgen.cpp @@ -286,10 +286,10 @@ int main(int argc, char *argv[]) { // Using disk file works well with klee-replay. create_stat(stdin_size, &s); - off64_t read_count = 0; + off_t read_count = 0; push_random_obj(&b, "stdin", stdin_size, stdin_size); push_obj(&b, "stdin-stat", sizeof(struct stat), (unsigned char *)&s); - push_obj(&b, "stdin-read", sizeof(off64_t), (unsigned char *)&read_count); + push_obj(&b, "stdin-read", sizeof(off_t), (unsigned char *)&read_count); } if (sym_stdout) { struct stat s; diff --git a/unittests/Expr/ArrayExprTest.cpp b/unittests/Expr/ArrayExprTest.cpp index f8049533a8..866e6d3fd7 100644 --- a/unittests/Expr/ArrayExprTest.cpp +++ b/unittests/Expr/ArrayExprTest.cpp @@ -16,7 +16,11 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/SourceBuilder.h" -#include +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP #include diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp index 8c7e1c1431..7cabaf8474 100644 --- a/unittests/Searcher/SearcherTest.cpp +++ b/unittests/Searcher/SearcherTest.cpp @@ -17,7 +17,11 @@ #include "Core/Searcher.h" #include "klee/ADT/RNG.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP using namespace klee; diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 8b15581dc0..3206bd1a18 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -16,7 +16,11 @@ #include "klee/Solver/Solver.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" +DISABLE_WARNING_POP #include diff --git a/unittests/TestMain.cpp b/unittests/TestMain.cpp index 9512e59a79..b6400d6630 100644 --- a/unittests/TestMain.cpp +++ b/unittests/TestMain.cpp @@ -7,8 +7,12 @@ // //===----------------------------------------------------------------------===// +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringRef.h" #include "llvm/Support/Signals.h" +DISABLE_WARNING_POP #include "gtest/gtest.h"