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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
