Hi,
I have a question about how string values are generated for symbolic
strings are generated in KLEE.
I am currently trying to test expr in Busybox. When I run KLEE with:
klee --libc=uclibc --posix-runtime --init-env busybox.bc --sym-arg 100
I get test-cases such as:
object 0: data:
'--help@\x00@@@@@@@@@@@@@?@@@@@@@@@@@@@@?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\x00'
object 0: data:
'--help??\x00@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@`\x00'
object 0: data:
'--help@@@\x00@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\x00'
object 0: data: '--help@@@@\x00@@@@@@@
@@@@@@@@@@@?@@@@@@@@@@@@@@?@@@@@?@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@`\x00'
I have 2 questions:
1. Can the characters after the \x00 null terminator effectively be
ignored? Is the effective input length the length of the string up to
the \x00 string terminator, if the program is reading input using
scanf("%s")?
2. If the effective input is everything in front of \x00, then why is
KLEE varying the characters after the first \x00?
3. Is "@" used as a random placeholder character for treating string
lengths rather than string contents as symbolic? Does KLEE have a
condition for deciding whether to treat the string contents as
symbolic or just the string length as symbolic? (ISSTA 2008, Testing
for buffer overflows with length abstraction.)
Thanks!
Jiaqi
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
