Re: [klee-dev] Dbg Location

2020-07-27 Thread Cristian Cadar 
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Dbg Location

2020-07-23 Thread Yugesh Kothari 
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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev