[klee-dev] KLEE as bitcode interpreter

Cristian Cadar c.cadar at imperial.ac.uk
Wed Mar 31 16:02:56 BST 2021


Yes, without any symbolic input, KLEE essentially functions like an 
interpreter for LLVM bitcode.

Best,
Cristian

On 19/03/2021 11:49, prashant chaturvedi wrote:
> Hi all.
>   I have compiled a source file to bitcode without debug information, 
> i'm not using "any" of the KLEE's intrinsic, i.e i'm not making anything 
> symbolic, just obtained a vanilla bitcode. If i run that bitcode in 
> KLEE, does KLEE here work llike  a bitcode interpreter? (like lli).  Is 
> it then really then same as running it on lli?
> 
> Thank you in advance!
> 
> _______________________________________________
> 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