added function name option on target pass

Author: Rafael Sá Menezes

modules/backend/pass/TargetPass.cpp

@@ -11,6 +11,12 @@
 #include "TargetPass.hpp"
 
 bool TargetPass::runOnFunction(Function& F) {
+  llvm::errs() << "Running TargetPass with: " << this->targetFunctionName;
+
+  // We need to have the definition of the function
+  F.getParent()->getOrInsertFunction(
+        this->targetFunctionName, Type::getVoidTy(F.getContext()));
+
   this->targetFunctionMap2Check = F.getParent()->getOrInsertFunction(
       "map2check_target_function", Type::getVoidTy(F.getContext()),
       Type::getInt8PtrTy(F.getContext()), Type::getInt32Ty(F.getContext()),

modules/backend/pass/TargetPass.hpp

@@ -19,6 +19,7 @@
 #include <llvm/IR/Module.h>
 #include <llvm/Pass.h>
 #include <llvm/Support/raw_ostream.h>
+#include <llvm/Support/CommandLine.h>
 
 #include <iostream>
 #include <sstream>
@@ -38,10 +39,15 @@ using llvm::IRBuilder;
 using llvm::LLVMContext;
 using llvm::RegisterPass;
 using llvm::Value;
+//using llvm::cl;
 
+// Target option
+static llvm::cl::opt<std::string> TargetNameOption("function-name", llvm::cl::desc("Specify the target function"), llvm::cl::init("__VERIFIER_error"));
 struct TargetPass : public FunctionPass {
   static char ID;
-  TargetPass() : FunctionPass(ID) {}
+  TargetPass() : FunctionPass(ID) {
+    targetFunctionName = TargetNameOption;
+  }
   explicit TargetPass(std::string FunctionName) : FunctionPass(ID) {
     targetFunctionName = FunctionName;
   }
@@ -56,7 +62,7 @@ struct TargetPass : public FunctionPass {
   BasicBlock::iterator currentInstruction;
   Constant *targetFunctionMap2Check = NULL;
   Value *functionName = NULL;
-  std::string targetFunctionName = "__VERIFIER_error";
+  std::string targetFunctionName;
 };
 
 #endif  // MODULES_BACKEND_PASS_TARGETPASS_HPP_

modules/frontend/caller.cpp

@@ -177,9 +177,10 @@ int Caller::callPass(std::string target_function, bool sv_comp) {
     }
     case Map2CheckMode::REACHABILITY_MODE: {
       Map2Check::Log::Info("Running reachability mode");
+      Map2Check::Log::Debug("Target function: " + target_function);
       std::string targetPass = "${MAP2CHECK_PATH}/lib/libTargetPass";
       transformCommand << " -load " << targetPass << getLibSuffix()
-                       << " -target_function";
+                       << " -target_function -function-name " << target_function;
 
       break;
     }

modules/frontend/map2check.cpp

@@ -302,7 +302,9 @@ int main(int argc, char **argv) {
 z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
         ("timeout", po::value<unsigned>(),
                       "\ttimeout for map2check execution")
-        ("target-function", "\tsearches for __VERIFIER_error is reachable")
+        ("target-function", "\tchecks wether <target-functions> is reachable")
+        ("target-function-name", po::value<std::string>()->default_value("__VERIFIER_error"),
+                      R"(define the function name to be searched)")
         ("generate-testcase", "\tcreates c program with fail testcase (experimental)")
         ("memtrack", "\tcheck for memory errors")
         ("print-counter", "\tprint counterexample")
@@ -371,7 +373,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))")
       args.timeout = timeout;
     }
     if (vm.count("target-function")) {
-      string function = "__VERIFIER_error";
+      string function = vm["target-function-name"].as<string>();
       args.function = function;
       args.mode = Map2Check::Map2CheckMode::REACHABILITY_MODE;
       args.spectTrue = "target-function";