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
