fix:

.github/workflows/build.yaml

@@ -6,6 +6,12 @@ on:
     branches: [main, utbot-main]
   push:
     branches: [main, utbot-main]
+  workflow_dispatch:
+    inputs:
+      logLevel:
+        description: 'Warnings as errors'
+        required: true
+        default: '1'
 
 # Defaults for building KLEE
 env:
@@ -17,7 +23,7 @@ env:
   ENABLE_DOXYGEN: 0
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
-  ENABLE_WARNINGS_AS_ERRORS: 0
+  ENABLE_WARNINGS_AS_ERRORS: {{ github.event.inputs.logLevel }}
   GTEST_VERSION: 1.11.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
   LLVM_VERSION: 11
@@ -57,7 +63,6 @@ jobs:
           "Latest klee-uclibc",
           "Asserts disabled",
           "No TCMalloc, optimised runtime",
-          "Warnings as errors",
         ]
         include:
           - name: "LLVM 16"
@@ -134,10 +139,6 @@ jobs:
               SOLVERS: STP
               USE_TCMALLOC: 0
               KLEE_RUNTIME_BUILD: "Release+Debug+Asserts"
-          # Check we can build without warnings
-          - name: "Warnings as errors"
-            env:
-              ENABLE_WARNINGS_AS_ERRORS: 1
     steps:
       - name: Checkout KLEE source code
         uses: actions/checkout@v3

build.sh

@@ -31,7 +31,7 @@ ENABLE_OPTIMIZED=1
 ENABLE_DEBUG=0
 DISABLE_ASSERTIONS=1
 REQUIRES_RTTI=1
-ENABLE_WARNINGS_AS_ERRORS=1
+ENABLE_WARNINGS_AS_ERRORS=0
 
 ## Solvers Required options
 # SOLVERS=STP
@@ -65,7 +65,6 @@ if [ "$1" = "--debug" ] || [ "$1" = "-g" ]; then
     ENABLE_OPTIMIZED=0
     ENABLE_DEBUG=1
     KLEE_RUNTIME_BUILD="Debug+Asserts"
-    ENABLE_WARNINGS_AS_ERRORS=0
     shift 1
 else
     KEEP_PARSE="false"

lib/Core/Memory.h

@@ -33,7 +33,6 @@ namespace klee {
 
 class BitArray;
 class ExecutionState;
-class Executor;
 class MemoryManager;
 class Solver;
 

lib/Core/SeedInfo.cpp

@@ -76,7 +76,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, ref<Expr> condition,
   std::set<std::pair<const Array *, unsigned>> directReads;
   std::vector<ref<ReadExpr>> reads;
   findReads(condition, false, reads);
-  for (auto const &re : reads) {
+  for (const auto &re : reads) {
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
       directReads.insert(
           std::make_pair(re->updates.root, (unsigned)CE->getZExtValue(32)));

test/regression/2023-11-20-solver.c

@@ -33,4 +33,4 @@ int main() {
   klee_assume(0 > p4);
   // CHECK: [[@LINE+1]]: ASSERTION FAIL
   assert(p2 > p11);
-}
+}

tools/kleaver/CMakeLists.txt

@@ -13,7 +13,8 @@ add_executable(kleaver
 llvm_config(kleaver "${USE_LLVM_SHARED}" core support)
 
 target_link_libraries(kleaver PRIVATE kleaverSolver)
-target_include_directories(kleaver SYSTEM PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS})
+target_include_directories(klee SYSTEM PRIVATE ${LLVM_INCLUDE_DIRS})
+target_include_directories(klee PRIVATE ${KLEE_INCLUDE_DIRS})
 target_compile_options(kleaver PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
 target_compile_definitions(kleaver PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
 

tools/klee/CMakeLists.txt

@@ -15,7 +15,8 @@ set(KLEE_LIBS
 )
 
 target_link_libraries(klee ${KLEE_LIBS})
-target_include_directories(klee SYSTEM PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS})
+target_include_directories(klee SYSTEM PRIVATE ${LLVM_INCLUDE_DIRS})
+target_include_directories(klee PRIVATE ${KLEE_INCLUDE_DIRS})
 target_compile_options(klee PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
 target_compile_definitions(klee PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
 

tools/klee/main.cpp

@@ -1491,7 +1491,6 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp,
     // Assume with early exit a bug finding mode and otherwise coverage
     if (UseGuidedSearch == Interpreter::GuidanceKind::ErrorGuidance)
       *meta_file << "\t<specification>COVER( init(main()), FQL(COVER "
-
                     "EDGES(@CALL(__VERIFIER_error))) )</specification>\n";
     else
       *meta_file << "\t<specification>COVER( init(main()), FQL(COVER "