[klee-dev] Symbolic pointers and memory allocation

Anitha B Gollamudi anitha.boyapati at gmail.com
Wed Apr 8 02:13:52 BST 2015


Hi,

When I try a simple program like the below, Klee gives me the error
"memory: invalid pointer make_symbolic".

The snippet is part of a larger testcase where I don't know the amount
of memory that I will
allocate to 'c'.  trying to test values of "c". Why is Klee unhappy?
How to fix without using arrays or malloc in such a situation?

int main() {

  char *c;
  klee_make_symbolic(c, sizeof(c), "c");
  return string_compare(c, "hello");
 }


-- 
 Anitha



More information about the klee-dev mailing list