Re: [klee-dev] Klee & pointers

2020-08-12 Thread Breger, Igor (Mobileye)
Hi Cristian, Thank you very much for the prompt reply. Regards, Igor -Original Message- From: klee-dev-boun...@imperial.ac.uk On Behalf Of Cristian Cadar Sent: Wednesday, August 12, 2020 17:19 To: klee-dev@imperial.ac.uk Subject: Re: [klee-dev] Klee & pointers Hi Igor, For this

Re: [klee-dev] Klee & pointers

2020-08-12 Thread Cristian Cadar
Hi Igor, For this example, I don't think it makes sense to make the pointer itself symbolic. You could instead replace the klee_make_symbolic call with klee_make_symbolic(a, sizeof(*a), "a"); to make the malloc'ed memory symbolic. If you're interested in symbolic pointers more generally, I

[klee-dev] Klee & pointers

2020-08-12 Thread Breger, Igor (Mobileye)
Hi all, I am trying to generate function coverage tests. From the tutorial and mail-archive I could not understand how I can define pointer as symbolic and also the data it point to. In the follow example, if I make a pointer symbolic, most of the tests KLEE generate are invalid ( 6 of 7 ) .