Re: [klee-dev] Add a C++ file for klee's POSIX library

2016-12-22 Thread Dan Liew
Hi,

On 22 December 2016 at 05:37, Randall  wrote:
> Hello eyeryone.
>
> I have met a problem while adding a c++ library which uses
> STL. So I get these error as follow:
>
> ...
>
> ...
>
> Unable to find size for global variable:  _ZNSs4_Rep20_S_empty_rep_storageE
> (use will result in out of bounds access)

KLEE does not support C++ properly so it's not surprising that this
doesn't work.

What is happening is that your program references
`std::basic_string::_Rep::_S_empty_rep_storage`
which is part of your compiler's C++ standard library (probably
libstdc++ or libcxx). KLEE does not ship with a LLVM bitcode version
of that library
and so at present it will trigger an out of bounds access if an
attempt is made to access it.


Thanks,
Dan.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] Add a C++ file for klee's POSIX library

2016-12-21 Thread Randall
Hello eyeryone.

I have met a problem while adding a c++ library which uses
STL. So I get these error as follow:

...

...

Unable to find size for global variable:  _ZNSs4_Rep20_S_empty_rep_storageE
(use will result in out of bounds access)

...

...

KLEE: ERROR:
/usr/lib/gcc/i686-linux-gnu/4.8/../../../../include/c++/4.8/ostream:565:
memory error: out of bound of pointer

KLEE: NOTE: now ignoring this error at this location

 

KLEE: done: total instructions = 4088

KLEE: done: completed paths = 1

KLEE: done: generated tests = 1

0  klee 0x08c22b1f llvm::sys::PrintStackTrace(_IO_FILE*) + 47

1  klee 0x08c22d8f

2  klee 0x08c22734

3   0xb774c400 __kernel_sigreturn + 0

4   0x09e55ed8 __kernel_sigreturn + 1383111384

Segment fault(core dump)

 

So I want to know what happened ?

 

Thanks in advance.

 

Randall

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev