[klee-dev] Klee and gmock error

[Martin Nowack]

Hi,

Two things:

> On 10 Sep 2015, at 16:31, Scholz, Niklas <niklas.scholz at tum.de> wrote:
> 
> KLEE: ERROR: /home/niklas/gmock-1.7.0/build/../gtest/src/gtest.cc:1667: memory error: out of bound pointer
> KLEE: NOTE: now ignoring this error at this location
> 
This is your first problem:
> ../gtest/src/gtest.cc:1667: memory error: out of bound pointer
There is an out-of-bound access there, please check the source code of gtest.
Maybe it’s intended, maybe there is another issue.
It might be part of the gmok startup routine, so whatever application you will link against it,
it will always fail. Please take a closer look to it to discover what could be the reason.
If it’s an issue with KLEE, please try to come up with a very small one-file test example (have a look at the test files under test/ directory).

> KLEE: done: total instructions = 815
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
> 0  libLLVM-3.4.so.1 0x00007f560a25c042 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
> 1  libLLVM-3.4.so.1 0x00007f560a25be34
> 2  libpthread.so.0  0x00007f560915f340
> 3  libpthread.so.0  0x0000000000e3f940
> Segmentation fault (core dumped)
Second, this segfault is a thing which worries me.
Despite any problem in your application, KLEE shouldn’t segfault.
(I assume here you use a vanilla KLEE)

Could you recompile KLEE, please make sure you use:
make DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 DEBUG_SYMBOLS=1

Run KLEE in a debugger and send me the stack trace.

Thanks,

Martin

> 
> Is there a way to use gmock and klee together? Thanks in advance.
> 
> Regards,
> Niklas
> 
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150911/b0848fee/attachment.sig>