[klee-dev] Adding klee_assert to LLVM IR

[Rasool Maghareh]

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