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 <[email protected]<mailto:[email protected]>> 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 [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
