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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
