search

nithishr / Klee-uClibcxx

Symbolic Execution for C++ using Klee
7 stars 2 forks source link

klee #1

Open Edward-L opened 6 years ago

Edward-L commented 6 years ago

i want use klee to run c++ code,but it dont work now, this is klee's configure ./configure \ LDFLAGS="-L$BUILDDIR/minisat/build/release/lib/" \ --with-llvm=$BUILDDIR/llvm-3.4.2.src/ \ --with-llvmcc=$BUILDDIR/llvm-3.4.2.src/Release/bin/clang \ --with-llvmcxx=$BUILDDIR/llvm-3.4.2.src/Release/bin/clang++ \ --with-stp=$BUILDDIR/stp/build/ \ --with-uclibc=$BUILDDIR/Klee-uClibcxx/klee-uClibcxx/Codes/klee-uClibc++ \ --with-z3=$BUILDDIR/z3/build/ \ --enable-cxx11 \ --enable-posix-runtime make -jnprocENABLE_OPTIMIZED=1 cp $BUILDDIR/z3/build/lib/libz3.so ./Release+Asserts/lib/ make install then i use clang++ general a bc file clang++ -emit-llvm -O0 -c map.cpp -o map.bc

finial i use klee to run it ,but it had some problem /app/Klee-uClibcxx/klee-uClibcxx/Codes/klee-c++/klee/Release+Asserts/bin/klee -libc=uclibc map.bc KLEE: ERROR: Link with library /app/Klee-uClibcxx/klee-uClibcxx/Codes/klee-c++/klee/Release+Asserts/lib/libuClibc++.a failed: Object file algorithm.o in archive is not supported is there any problem?

Edward-L commented 6 years ago

oh , i also builda lib folder in Codes/klee-uClibc++ and move libuClibc++.a in it