Hello all,
I am adding klee_assert manually to LLVM IR. I notice that KLEE
terminates the paths
when reaching klee_assert. However, if I add klee_assert to the C code
before
compilation KLEE continues the path to the end after reaching the
klee_assert.
This is important for me since sometimes a path violates more than one
klee_assert
and I want KLEE to catch them all.
I have tried both with and without --emit-all-errors, but problem exists.
I am using the following code to create the call to the assert_fail
function.
//new fail basic block
llvm::BasicBlock *fail =
llvm::BasicBlock::Create(llvm::getGlobalContext(),"fail", &F);
llvm::IRBuilder<> builder2(fail);
//begin of klee_assert
llvm::Constant *c = M->getOrInsertFunction(
"__assert_fail",
llvm::FunctionType::getVoidTy(F.getContext()),
llvm::Type::getInt8PtrTy(F.getContext()),
llvm::Type::getInt8PtrTy(F.getContext()),
llvm::IntegerType::get(llvm::getGlobalContext(), 32),
llvm::Type::getInt8PtrTy(F.getContext()),
NULL);
llvm::Function *assert_fail = llvm::dyn_cast<llvm::Function>(c);
llvm::Value *message = builder2.CreateGlobalStringPtr(msgString, ".str");
llvm::Value *file = builder2.CreateGlobalStringPtr("",".str");
llvm::ConstantInt *line = builder2.getInt32(0);
llvm::Value *function = builder2.CreateGlobalStringPtr("main",".str");
builder2.CreateCall4(assert_fail, message, file,line, function);
I would be thankful if anyone can help informing which part I am doing
incorrectly.
Thanks & Regards
Rasool
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
