Hi, On 22 December 2016 at 05:37, Randall <xyhbg920...@163.com> 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<char, std::char_traits<char>, std::allocator<char> >::_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