Receive instrumented revision number

1 files changed, 15 insertions, 0 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 332e4b56..e67a1676 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -107,6 +107,7 @@ static SpecialFunctionHandler::HandlerInfo 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),
@@ -873,3 +874,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();
+}