[klee-dev] Same variable twice in ktest-tool output

[Sean Bartell]

Hi,

Alexander Kampmann on 2015-06-25:
>For my test input, the ktest-tool outputs the same object name twice and
>skips another object.

>As you can see, there are two objects named 'var2' and no object named
>'var1'. The c code is:

>        char *var1 = "Hallo";
>        char *var2 = "Hallo";
>        klee_make_symbolic(var1, 6*sizeof(char), "var1");
>        klee_assume(var1[5] == 0);
>        klee_make_symbolic(var2, 6*sizeof(char), "var2");
>        klee_assume(var2[5] == 0);

"Hallo" is a string constant, and the compiler puts it in read-only memory. 
Because it's read-only, the compiler is allowed to combine both instances of 
"Hallo" to save memory. You aren't supposed to treat the string constants as 
writable and if you compile with -Wall you'll get a warning to that effect. 
klee_make_symbolic essentially writes to the read-only memory and that is 
causing issues.

What you really want is this:

  char var1[] = {"Hallo"};
  char var2[] = {"Hallo"};

Both variables will get separate instances of "Hallo" in writable memory, so 
KLEE should work as expected.

It's interesting that KLEE gets the names confused. I guess it fills the string 
constant with symbolic values, then overwrites those symbolic values with *new* 
symbolic values, and also overwrites the old name for that memory location with 
the new name. You see both sets of symbolic values, but KLEE only remembers the 
new name for them.