[klee-dev] Symbolic pointers and memory allocation

[Jonathan Neuschäfer]

On Tue, Apr 07, 2015 at 09:13:52PM -0400, Anitha B Gollamudi wrote:
> 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");
>  }

You're trying to generate a wild pointer -- it could point to anything
if concretized. Something like the following should work:

int main() {
	int len = 42;	/* maximum length */
	char *string = malloc(len);
	klee_make_symbolic(string, len, "c");
	return strcmp(string, "hello");
}


I hope that helps,
  Jonathan Neuschäfer