[feat] Add mocks

UnitTestBot · Apr 30, 2023 · 36ee656 · 36ee656
1 parent 6983578
commit 36ee656
Show file tree

Hide file tree

Showing 9 changed files with 332 additions and 157 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -52,7 +52,7 @@ jobs:
                 "Latest klee-uclibc",
                 "Asserts enabled",
                 "No TCMalloc, optimised runtime",
-            ]
+              ]
         include:
           - name: "LLVM 13"
             env:

diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h
@@ -33,7 +33,8 @@
   TTYPE(ReadOnly, 17U, "read_only.err")                                        \
   TTYPE(ReportError, 18U, "report_error.err")                                  \
   TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err")                      \
-  MARK(PROGERR, 19U)                                                           \
+  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er")                          \
+  MARK(PROGERR, 20U)                                                           \
   TTYPE(User, 23U, "user.err")                                                 \
   MARK(USERERR, 23U)                                                           \
   TTYPE(Execution, 25U, "exec.err")                                            \

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
@@ -87,6 +87,7 @@ ExecutionState::ExecutionState(KFunction *kf)
     : initPC(kf->instructions), pc(initPC), prevPC(pc),
       roundingMode(llvm::APFloat::rmNearestTiesToEven) {
   pushFrame(nullptr, kf);
+  setID();
 }
 
 ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
@@ -346,6 +347,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
 
   std::set<ref<Expr>> aConstraints(constraints.begin(), constraints.end());
   std::set<ref<Expr>> bConstraints(b.constraints.begin(), b.constraints.end());
+
   std::set<ref<Expr>> commonConstraints, aSuffix, bSuffix;
   std::set_intersection(
       aConstraints.begin(), aConstraints.end(), bConstraints.begin(),
@@ -357,6 +359,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
   std::set_difference(bConstraints.begin(), bConstraints.end(),
                       commonConstraints.begin(), commonConstraints.end(),
                       std::inserter(bSuffix, bSuffix.end()));
+
   if (DebugLogStateMerge) {
     llvm::errs() << "\tconstraint prefix: [";
     for (std::set<ref<Expr>>::iterator it = commonConstraints.begin(),
@@ -472,6 +475,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
   constraints = ConstraintSet();
 
   ConstraintManager m(constraints);
+
   for (const auto &constraint : commonConstraints)
     m.addConstraint(constraint);
   m.addConstraint(OrExpr::create(inA, inB));