Dear all, as preliminary remarks, I have no idea if the following issues are related to my tiny knowledge of the tool.
At the moment I am running the svn-HEAD klee as follows. The ferguson.c code is hereby attached. # clang -I $KLEE_HOME/include/ -g -c -emit-llvm ../src/ferguson.c -o ferguson.bc # klee -time-max 3600 ferguson.bc ... thousand of paths are covered ... # klee -optimize ferguson.bc KLEE: output directory = "klee-out-5" WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts! KLEE: done: total instructions = 13 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 Why does the -optimize flag produce poor results? What are these WARNING messages? Best regards, Giuseppe -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100426/d9bdf6f9/attachment.html -------------- next part -------------- A non-text attachment was scrubbed... Name: ferguson.c Type: application/octet-stream Size: 1859 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100426/d9bdf6f9/attachment.obj
