Receive instrumented revision number

1 files changed, 15 insertions, 0 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index b0c28fbc..784bb8f1 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -109,6 +109,7 @@ static constexpr std::array handlerInfo = {
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
+  add("klee_mark_patch", handleMarkPatch, false),
   add("klee_open_merge", handleOpenMerge, false),
   add("klee_close_merge", handleCloseMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
@@ -840,3 +841,17 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
+
+void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state,
+                                             KInstruction *target,
+                                             std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 1 &&
+         "invalid number of arguments to klee_mark_patch");
+  assert(isa<ConstantExpr>(arguments[0]) &&
+         "expect constant patch number argument to klee_mark_patch");
+  if (state.patchNo)
+    executor.terminateStateEarly(state, "ignore patch combination",
+                                 StateTerminationType::SilentExit);
+  else
+    state.patchNo = cast<ConstantExpr>(arguments[0])->getLimitedValue();
+}