Thanks. On 06/25/2015 04:26 PM, Paul Marinescu wrote: > 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 <[email protected]> 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
