[klee-dev] Klee & pointers

[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 ) . 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.
-------------- next part --------------
HTML attachment scrubbed and removed