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

[Paul Marinescu]

KLEE should handle this more gracefully. I’ve opened an issue on your behalf at https://github.com/klee/klee/issues/248

Paul

> On 25 Jun 2015, at 14:49, Sean Bartell <sean at yotann.org> wrote:
> 
> 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.
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev