Hi,
I met a problem when I used the following command line to generate test
cases:klee --libc=uclibc --posix-runtime --max-time=60 print_tokens.o A
--sym-files 1 36(Originally there is an --init-env option, but klee complained
that the option doesn't exist)The program print_tokens simply reads from the
input file and print tokens to the stdout. (It's the print_tokens program in
the Siemens suite)But it seems that when running in klee with the above command
line, none of the instances of print_tokens can exit normally. I get 3
files(.early, .pc and .ktest) for each test case klee generated.And in 60
seconds, klee only generated about 10 test cases, covering very few paths.
This is a typical output of klee:KLEE: NOTE: Using model:
/home/shoreray/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bcaKLEE: output
directory = "klee-out-3"KLEE: WARNING: undefined reference to function:
__xstat64KLEE: WARNING: undefined reference to function: klee_get_valuelKLEE:
WARNING: executable has module level assembly (ignoring)KLEE: WARNING: calling
external: syscall(54, 0, 21505, 190205144)KLEE: WARNING: calling __user_main
with extra arguments.KLEE: WARNING: calling external: __xstat64(3, 190144720,
190292400)KLEE: WARNING: ioctl: (TCGETS) symbolic file, incomplete modelKLEE:
HaltTimer invokedKLEE: halting execution, dumping remaining states
KLEE: done: total instructions = 15576KLEE: done: completed paths = 9KLEE:
done: generated tests = 9
A test case generated may look like:ktest file : 'test000004.ktest'args :
['print_tokens.o', 'A', '--sym-files', '1', '36']num objects: 5object 0:
name: 'A-data'object 0: size: 36object 0: data:
'a\n\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'object
1: name: 'A-data-stat'object 1: size: 96object 1: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x005\x1ezP\x00\x00\x00\x00R
zP\x00\x00\x00\x00R zP\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'object
2: name: 'stdin'object 2: size: 36object 2: data:
'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'object
3: name: 'stdin-stat'object 3: size: 96object 3: data:
'\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x005\x1ezP\x00\x00\x00\x00R
zP\x00\x00\x00\x00R zP\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff'object
4: name: 'model_version'object 4: size: 4object 4: data:
'\x01\x00\x00\x00'
For the test case above, I thought the program should output an "a". But
strangely, no output is observed when klee was running.
I got confused about klee's behavior. Could someone please help me out?
Many thanks.
Shoreray
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
