[klee-dev] Facing a problem in linking the external library with KLEE

[Nowack, Martin]

Hi,

It looks like there is a problem for KLEE with some unsupported globals and their properties.
Can you open an issue https://github.com/klee/klee/issues ?

And we can continue the discussion there.

One small remark, please don’t send images containing text - instead, copy the text into the email.
Thanks a lot.

Cheers,
Martin


On 3. Jul 2019, at 06:31, Muhammad Monir Hossain <monir.eee.buet at gmail.com<mailto:monir.eee.buet at gmail.com>> wrote:

Dear concern,

Greetings! Hope you are doing well!

I write a code using LLVM dataflow sanitizer library and KLEE assertion and then convert it to LLVM bit-code. I run the bit-code with KLEE and get some errors. Here, I have attached the code and screenshot about errors/output from the tools I received.

Code:
<image.png>

The output from KLEE:
<image.png>

Would you please let me know why Klee can't run that LLVM bit-code? Is there any problem with libclang_rt.dfsan-x88_64.a static library? Do I need to use the LLVM bit-code of this library or a shared library (.so) or anything else I need to do?

I am eagerly waiting for your kind reply. Thank you.


Sincerely,

Muhammad Monir Hossain

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed