[klee-dev] Klee & pointers

[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 would 
recommend this paper, which contains in the beginning a discussion of 
the different memory models used in symbolic execution (as well as 
proposing a new model):
https://srg.doc.ic.ac.uk/publications/19-segmem-esecfse.html

Best,
Cristian

On 09/08/2020 14:45, Breger, Igor (Mobileye) wrote:
> 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 ) . The only valid test is with NULL 
> values.
> 
> I would appreciate any help.
> 
> Best Regards,
> 
> Igor
> 
> #include "klee/klee.h"
> 
> #include <stdlib.h>
> 
> int get_sign(int *a) {
> 
>    if ( a == NULL)
> 
>      return 2;
> 
>    int x = *a;
> 
>    if (x == 0)
> 
>      return 0;
> 
>    if (x < 0)
> 
>      return -1;
> 
>    else
> 
>      return 1;
> 
> }
> 
> int main() {
> 
>    int *a = (int*)malloc(sizeof(int));
> 
>    klee_make_symbolic(&a, sizeof(a), "a");
> 
>    return get_sign(a);
> 
> }
> 
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>