Fixes after rebase

UnitTestBot · Oct 6, 2023 · 5736c61 · 5736c61
1 parent ef6ff72
commit 5736c61
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 19 deletions.
diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h
@@ -109,6 +109,8 @@ class IndependentConstraintSet {
 
   InnerSetUnion concretizedSets;
 
+  std::set<std::string> uninterpretedFunctions;
+
   ref<const IndependentConstraintSet> addExpr(ref<Expr> e) const;
   ref<const IndependentConstraintSet>
   updateConcretization(const Assignment &delta,

diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h
@@ -88,7 +88,7 @@ struct AllocSource final : public Unknown {
 struct Free final : public Unknown {
 public:
   enum Type {
-    Free_ = 1,           // Kind of free function
+    Free_ = 1,          // Kind of free function
     Delete = 2,         // operator delete
     DeleteBrackets = 3, // operator delete[]
     CloseFile = 4,      // close file

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
@@ -1002,8 +1002,8 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
                                      executor.updateNameVersion(state, name));
         break;
       case MockStrategy::Deterministic:
-        std::vector<ref<Expr>> args(kf->numArgs);
-        for (size_t i = 0; i < kf->numArgs; i++) {
+        std::vector<ref<Expr>> args(kf->getNumArgs());
+        for (size_t i = 0; i < kf->getNumArgs(); i++) {
           args[i] = executor.getArgumentCell(state, kf, i).value;
         }
         source = SourceBuilder::mockDeterministic(executor.kmodule.get(),

diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp
@@ -277,13 +277,11 @@ bool IndependentConstraintSet::intersects(
     if (it2 != b->elements.end()) {
       if (it->second.intersects(it2->second)) {
         return true;
+      }
     }
-  }
-  for (std::set<std::string>::iterator it = uninterpretedFunctions.begin(),
-                                       ie = uninterpretedFunctions.end();
-       it != ie; ++it) {
-    if (b.uninterpretedFunctions.count(*it)) {
-      return true;
+    for (const auto &uFn : a->uninterpretedFunctions) {
+      if (b->uninterpretedFunctions.count(uFn)) {
+        return true;
       }
     }
   }

diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
@@ -623,8 +623,8 @@ SourceResult ParserImpl::ParseMockDeterministicSource() {
   ConsumeExpectedToken(Token::Identifier);
   ConsumeLParen();
   std::vector<ref<Expr>> args;
-  args.reserve(kf->numArgs);
-  for (unsigned i = 0; i < kf->numArgs; i++) {
+  args.reserve(kf->getNumArgs());
+  for (unsigned i = 0; i < kf->getNumArgs(); i++) {
     auto expr = ParseExpr(TypeResult());
     if (!expr.isValid()) {
       return {false, nullptr};

diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp
@@ -164,7 +164,7 @@ unsigned InstructionSource::computeHash() {
 
 unsigned MockNaiveSource::computeHash() {
   unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version;
-  unsigned funcID = km->functionIDMap.at(&function);
+  unsigned funcID = km->getFunctionId(&function);
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID;
   hashValue = res;
   return res;
@@ -178,8 +178,8 @@ int MockNaiveSource::internalCompare(const SymbolicSource &b) const {
   if (version != mnb.version) {
     return version < mnb.version ? -1 : 1;
   }
-  unsigned funcID = km->functionIDMap.at(&function);
-  unsigned bFuncID = mnb.km->functionIDMap.at(&mnb.function);
+  unsigned funcID = km->getFunctionId(&function);
+  unsigned bFuncID = mnb.km->getFunctionId(&mnb.function);
   if (funcID != bFuncID) {
     return funcID < bFuncID ? -1 : 1;
   }
@@ -194,7 +194,7 @@ MockDeterministicSource::MockDeterministicSource(
 unsigned MockDeterministicSource::computeHash() {
   unsigned res = getKind();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(&function);
+        km->getFunctionId(&function);
   for (const auto &arg : args) {
     res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash();
   }
@@ -208,8 +208,8 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const {
   }
   const MockDeterministicSource &mdb =
       static_cast<const MockDeterministicSource &>(b);
-  unsigned funcID = km->functionIDMap.at(&function);
-  unsigned bFuncID = mdb.km->functionIDMap.at(&mdb.function);
+  unsigned funcID = km->getFunctionId(&function);
+  unsigned bFuncID = mdb.km->getFunctionId(&mdb.function);
   if (funcID != bFuncID) {
     return funcID < bFuncID ? -1 : 1;
   }

diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
@@ -92,11 +92,11 @@ template <> void Z3NodeHandle<Z3_sort>::dump() const __attribute__((used));
 template <> unsigned Z3NodeHandle<Z3_sort>::hash() __attribute__((used));
 
 // Specialize for Z3_func_decl
-template <> inline ::Z3_ast Z3NodeHandle<Z3_func_decl>::as_ast() {
+template <> inline ::Z3_ast Z3NodeHandle<Z3_func_decl>::as_ast() const {
   return ::Z3_func_decl_to_ast(context, node);
 }
 typedef Z3NodeHandle<Z3_func_decl> Z3FuncDeclHandle;
-template <> void Z3NodeHandle<Z3_func_decl>::dump() __attribute__((used));
+template <> void Z3NodeHandle<Z3_func_decl>::dump() const __attribute__((used));
 
 // Specialise for Z3_ast
 template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() const {