Hi, Both test cases (CXX/StaticDestructor.cpp and Feature/WriteCov.c) fail on my Mac (LLVM 2.7 + KLEE SVN HEAD + Darwin 10.5.0) since they grep for a "file:line" string which is not generated by KLEE. For some reasons, ii.file() in Executor::terminateStateOnError appears to be empty generating the error message without file:line information, e.g. for StaticDestructor:
... KLEE: ERROR: memory error: out of bound pointer ... On a Linux machine the test case passes because the line information is included: ... KLEE: ERROR: /some/path/CXX/StaticDestructor.cpp:16: memory error: out of bound pointer ... Any ideas why ii.file() is empty? In contrast, ii.line() contains the right line number as expected. Thanks, Raimondas -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 4409 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20101202/356dcb7c/attachment.bin
