[klee-dev] Is it possible to use llvm bitcode lines as target for klee evaluation?

Cadar, Cristian c.cadar at imperial.ac.uk
Tue Aug 20 11:27:54 BST 2019


There's no such support in mainline KLEE, but you can look at KATCH for 
such an extension (https://srg.doc.ic.ac.uk/publications/13-katch-fse.html).

Cristian

On 16/08/2019 03:35, Arnab Kumar Biswas wrote:
> I have a couple of llvm bitcode lines that I have already identified as 
> possible targets. Is there any way to use them as target for klee 
> evaluation? Basically, I want klee to reach those lines as fast as 
> possible instead of going in different directions or branches. If there 
> is any existing project or paper, kindly let me know.
> 
> 
> ------------------------------------------------------------------------
> 
> Important: This email is confidential and may be privileged. If you are 
> not the intended recipient, please delete it and notify us immediately; 
> you should not copy or use it for any purpose, nor disclose its contents 
> to any other person. Thank you.
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 


More information about the klee-dev mailing list