[klee-dev] Adding klee_assert to LLVM IR

[Daniel Schemmel]

Hi Rasool,

as `__assert_fail` is a KLEE special function (see
[`lib/Core/SpecialFunctionHandler.cpp`](https://github.com/klee/klee/blob/0f1b68e093dfe0357adf400ea7b4746f09fb4cba/lib/Core/SpecialFunctionHandler.cpp#L73)),
you cannot override it in LLVM IR. Your function simply will not be
called by KLEE.

If you wish to change the behavior of KLEE, either change the Special
Function, or change the macro `klee_assert` to something that does what
you require of it.

Greetings,
Daniel

On 9/3/2018 7:29 AM, Rasool Maghareh wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev