Dear Hailong,

It seems that the library "librt" is not being linked correctly. What you can 
do is to explicitly tell to the Makefile to link to this library by adding 
"-lrt". When compiling you should see something like this: "gcc file.c ... 
-lrt".

Regards,
Javier


________________________________
From: Hailong Yang [[email protected]]
Sent: 28 September 2012 02:00
To: [email protected]
Subject: installation problems with software-testing

Dear All,

I am installing the software-testing benchmark on a Ubuntu 12.04.1 machine. 
However, when I am building Cloud9, I got the following error:

make[2]: Leaving directory 
`/home/hailong/software_testing/cloud9/stp/simplifier'
make[1]: Leaving directory `/home/hailong/software_testing/cloud9/stp'
make[1]: Entering directory `/home/hailong/software_testing/cloud9/tools'
make[2]: Entering directory `/home/hailong/software_testing/cloud9/tools/klee'
llvm[2]: Compiling Debug.cpp for Release+Asserts build
llvm[2]: Compiling main.cpp for Release+Asserts build
llvm[2]: Linking Release+Asserts executable klee (without symbols)
/home/hailong/software_testing/cloud9/Release+Asserts/lib/libkleeCore.a(TimingSolver.o):
 In function `cloud9::instrum::Timer::start()':
/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:97: 
undefined reference to `clock_gettime'
/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:102: 
undefined reference to `clock_gettime'
/home/hailong/software_testing/cloud9/Release+Asserts/lib/libkleeCore.a(TimingSolver.o):
 In function `cloud9::instrum::Timer::stop()':
/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:111: 
undefined reference to `clock_gettime'
/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:116: 
undefined reference to `clock_gettime'
/home/hailong/software_testing/cloud9/Release+Asserts/lib/libkleeCore.a(TimingSolver.o):
 In function `cloud9::instrum::Timer::start()':
/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:97: 
undefined reference to `clock_gettime'
/home/hailong/software_testing/cloud9/Release+Asserts/lib/libkleeCore.a(TimingSolver.o):/home/hailong/software_testing/cloud9/include/cloud9/instrum/Timing.h:102:
 more undefined references to `clock_gettime' follow
collect2: ld returned 1 exit status
make[2]: *** [/home/hailong/software_testing/cloud9/Release+Asserts/bin/klee] 
Error 1
make[2]: Leaving directory `/home/hailong/software_testing/cloud9/tools/klee'
make[1]: *** [klee/.makeall] Error 2
make[1]: Leaving directory `/home/hailong/software_testing/cloud9/tools'
make: *** [all] Error 1

It seems the library is not linked correctly. Anyone knows how to fix it?

Best

Hailong

Reply via email to