Hi again! On Wed, Jul 29, 2009 at 10:59 AM, Vladimir Kuznetsov<ks.vladimir at gmail.com> wrote: > 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.
Ok, as mentioned in my previous email this is a nasty issue I'd like to look closer at. It would be nice to detect actual errors when this occurs and is unsafe, but since > - 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. Ok, this ones easy, if you send the patch I'll drop it in. > - 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. Can you file a bug for this with a test case? I should get to it at some point... Thanks again, - Daniel > First two bugs are fixed in my 64bit port of KLEE, but the last one is not. > > -- > With the best regards, > Vladimir > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
