[klee-dev] Dbg Location

Cristian Cadar c.cadar at imperial.ac.uk
Mon Jul 27 13:09:56 BST 2020


KLEE performs various transformations & optimizations on the input 
bitcode file, which is why you see those differences.

Best,
Cristian

On 23/07/2020 09:55, Yugesh Kothari wrote:
> Hi,
> 
> I had a question about the dbg location as seem in the assembly.ll file 
> generated by Klee.
> I assume that Klee operates on this assembly.ll file (so please correct 
> me if wrong).
> 
> I was comparing the dbg location information printed in assembly.ll and 
> the .ll file generated by running llvm-dis input.bc and found them to be 
> different. I was wondering why this is the case?
> 
> Thanks!
> 
> _______________________________________________
> 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