From ba084db1ab0307d96d7cae0fa087eb0c6d6f3679 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <mcsinyx@disroot.org>
Date: Thu, 30 Mar 2023 19:57:43 +0900
Subject: Receive instrumented revision number

---
 lib/Core/SpecialFunctionHandler.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'lib/Core/SpecialFunctionHandler.cpp')

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();
+}
-- 
cgit 1.4.1