Rebase fixes

UnitTestBot · Jan 15, 2024 · 97cb313 · 97cb313
1 parent c30d262
commit 97cb313
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 9 deletions.
diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h
@@ -7,14 +7,12 @@
 #include "vector"
 
 #include "nlohmann/json.hpp"
-#include "nonstd/optional.hpp"
+#include <optional>
 
 #include "klee/Config/config.h"
 
 #include "llvm/IR/Module.h"
 
-using nonstd::nullopt;
-using nonstd::optional;
 using json = nlohmann::json;
 
 namespace klee {

diff --git a/include/klee/Module/SarifReport.h b/include/klee/Module/SarifReport.h
@@ -18,7 +18,7 @@
 
 #include "klee/ADT/Ref.h"
 #include "llvm/IR/Function.h"
-#include <nlohmann/json.hpp>
+#include "nlohmann/json.hpp"
 
 using json = nlohmann::json;
 

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
@@ -994,7 +994,7 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
       switch (executor.interpreterOpts.MockStrategy) {
       case MockStrategyKind::Naive:
         source =
-            SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function,
+            SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function(),
                                      executor.updateNameVersion(state, name));
         break;
       case MockStrategyKind::Deterministic:
@@ -1003,7 +1003,7 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
           args[i] = executor.getArgumentCell(state, kf, i).value;
         }
         source = SourceBuilder::mockDeterministic(executor.kmodule.get(),
-                                                  *kf->function, args);
+                                                  *kf->function(), args);
         break;
       }
       executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source,

diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
@@ -646,7 +646,7 @@ SourceResult ParserImpl::ParseMockNaiveSource() {
   auto versionExpr = ParseNumber(64).get();
   auto version = dyn_cast<ConstantExpr>(versionExpr);
   assert(version);
-  return SourceBuilder::mockNaive(km, *kf->function, version->getZExtValue());
+  return SourceBuilder::mockNaive(km, *kf->function(), version->getZExtValue());
 }
 
 SourceResult ParserImpl::ParseMockDeterministicSource() {
@@ -664,7 +664,7 @@ SourceResult ParserImpl::ParseMockDeterministicSource() {
     args.push_back(expr.get());
   }
   ConsumeRParen();
-  return SourceBuilder::mockDeterministic(km, *kf->function, args);
+  return SourceBuilder::mockDeterministic(km, *kf->function(), args);
 }
 
 SourceResult ParserImpl::ParseAlphaSource() {

diff --git a/test/Industry/BadCase01_SecB_ForwardNull.c b/test/Industry/BadCase01_SecB_ForwardNull.c
@@ -142,6 +142,6 @@ void badbad(char *ptr)
 
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc > %t1.log 2>&1
 // RUN: FileCheck -input-file=%t1.log %s
 // CHECK: KLEE: WARNING: No paths were given to trace verify