[klee-dev] Analysis klee error for lifted x86 code

[kmohit]

Hi,

   I am trying to lift a code for x86 architecture and later run it on Klee-2.1.
So that, Klee analysis it and gives which type of error is it. But it is not
giving that error which is expected.
For example, here written a code for free.err but when we try to lift it and
analysis it with Klee it gives me out bound error i.e ptr.err.
 Could you help in this problem or give me any examples for that. Here the code
,



#include <stdlib.h>

   int global[3];
   int main(void)
             {
                    free(global); // free.err
                    break;
               }

Thanks in advance...


Best,
Mohit

For assimilation and dissemination of knowledge, visit cakes.cdac.in 


------------------------------------------------------------------------------------------------------------
[ C-DAC is on Social-Media too. Kindly follow us at:
Facebook: https://www.facebook.com/CDACINDIA & Twitter: @cdacindia ]

This e-mail is for the sole use of the intended recipient(s) and may
contain confidential and privileged information. If you are not the
intended recipient, please contact the sender by reply e-mail and destroy
all copies and the original message. Any unauthorized review, use,
disclosure, dissemination, forwarding, printing or copying of this email
is strictly prohibited and appropriate legal action will be taken.
------------------------------------------------------------------------------------------------------------

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.jpg
Type: image/jpeg
Size: 7789 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210531/57a73eb3/attachment.jpg>