Hello, During porting KLEE to 64bit I have found several bugs that affects also 32bit KLEE. Here is a list:
- When calling a function, types of actual arguments may not always match with types that function expects. Example: %0 = call i32 (...)* bitcast (i32 (i32)* @islower to i32 (...)*) (i16 97) The code runs fine in lli, but leads to an assertion failure in KLEE. On 64bit platforms llvm-gcc generates such code quite often, mainly when a function expects 64bit argument but is invoked with 32bit one. - In runAndGetCexForked() function KLEE does not check for EINTR error when calling waitpid. On 64bit it leads to an assertion failure in some situations. The problem may also be visible on some 32bit systems. - Currently KLEE does not support "byval" parameter attribute. llvm-gcc generates a code using this attribute when a function has many arguments (although I do not know for sure what is the threshold). A testcase to trigger the bug is in the attached file. Other LLVM parameter attributes are not supported either and may also cause problems. First two bugs are fixed in my 64bit port of KLEE, but the last one is not. -- With the best regards, Vladimir -------------- next part -------------- A non-text attachment was scrubbed... Name: byval_bug.c Type: text/x-csrc Size: 833 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090729/35d13b11/attachment.bin
