[klee-dev] C++ Support Status

[Daniel Schemmel]

Hello Volodomyr,

C++ support in KLEE is available, with the major caveat that (as for C 
code) you need to compile everything to LLVM bitcode. Just like for C 
code, we have a prepared standard library available, although there are 
some limitations in that regard (again, just as for C). The biggest 
issue is that we do not currently perform a lot of tests using C++ code, 
and the user-base that uses KLEE on C code is much bigger.

For your example, this means that you need to provide LLVM bitcode for 
your code as well as the gtest library. Both of them should be built 
against our standard library, or you will have to provide your own 
standard library as well (which is a pain). Your code looks to me like 
it might build your own project as bitcode, but try to link against a 
binary google test version and it does not deal especially with the 
standard library location (which in theory could be set up in such a way 
that it is unnecessary, but that is probably not the case).

Best,
Daniel

On 2024-04-13 09:47, Volodymyr Melnychenko wrote:
>
> Hello,
>
> Is Klee a good tool for analyzing C++ code?  I saw an email from 2018 
> regarding C++,  what's progress on it? Do you have examples of using 
> Klee in C++ projects with CMake, Qt, Boost, STL, Google Test, etc?
>
> I just started to go through examples. I set compiler and linker flags 
> as follows:
>
> add_compile_options(-flto -emit-llvm -Xclang -disable-O0-optnone)
> set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS}-flto 
> -Wl,-plugin-opt=emit-llvm")
>
>
> Does it look correct? I want to compile a Google Test project for a 
> start consisting of only two cpp files and a few tests.
>
>
> Main function is typical:
>
> int main(int argc,char **argv) {
>    testing::InitGoogleTest(&argc, argv);
>    return RUN_ALL_TESTS();
> }
>
> Now gtest runs and executes all tests successfully. Running Klee 
> gives  me this:
>
> KLEE: WARNING: executable has module level assembly (ignoring)
> KLEE: ERROR: Unable to load symbol(_ZTIN7testing4TestE) while 
> initializing globals
>
> Thanks!
>
>
> -- 
> Regards,
> Volodymyr Melnychenko
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed