[klee-dev] KLEE for C++ programs using pthreads.

[Cristian Cadar]

Hi Dilip,

Currently, KLEE has limited support for C++, and no support for 
pthreads.  However, there are certain extensions to KLEE that handle 
these aspects, e.g., KLOVER for C++ and Cloud9 for pthreads.  Take a 
look at http://klee.llvm.org/Publications.html for more information.

Cristian

On 06/01/13 19:20, Dilip Murali wrote:
> Hello Klee developers,
>
> I am a beginner trying to use KLEE.
> I am using the KLEE self contained package to on a C++ program that
> uses pthreads.
> I have generated a .o file and used KLEE with the following option
>
> klee --libc=uclibc --posix-runtime test.o
>
> But i see i get warning
>
> KLEE: NOTE: Using model:
> /home/pgbovine/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-4"
> KLEE: WARNING: undefined reference to function: klee_get_valuel
> KLEE: WARNING: undefined reference to function: pthread_create
> KLEE: WARNING: undefined reference to function: pthread_exit
> KLEE: WARNING: undefined reference to function: pthread_join
> KLEE: WARNING: executable has module level assembly (ignoring)
> KLEE: WARNING: calling external: syscall(54, 0, 21505, 571522624)
> KLEE: WARNING: calling __user_main with extra arguments.
> KLEE: WARNING: calling external: pthread_create(571589384, 0,
> 563903904, 571574176)
> 0  klee 0x08965ab8
> [pid  1846] +++ killed by SIGSEGV +++
> +++ killed by SIGSEGV +++
> Segmentation fault
>
> Using klee on a .bc file also gives me the same result.
>
> I am not sure why i get undefined reference to pthread functions. I am
> not sure if the libraries for pthreads are being used properly. Is
> there a way to ensure this? Using the llvm-ld also does not help.
> Below is the llvm-ld command that i used
>   llvm-ld tests.bc -l=/usr/lib/libpthread.a
>
> I am not sure why there Segmentation fault occurs. The program works
> fine when i normally compile the programs with g++ and run  the
> executable file.
>
>
> Could someone tell me where i am going wrong?
>
> Thanks & Regards,
> Dilip
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>