ThanhVu (Vu) Nguyen
2014-02-12 02:12:15 UTC
Hi,
I try to build Klee using the instruction from this page
http://ccadar.github.io/klee/GetStarted.html . I was not able to build
stp-r940.tgz, after doing "make OPTIMIZE=-O2 CFLAGS_M32= install" , I get
error about AssertsQuery not declared in scope (see [1]). So I try the
latest version of stp as suggested from this message
http://www.mail-archive.com/klee-dev-AQ/***@public.gmane.org/msg01315.html . I was
able to build this stp version fine with the make command "make
CFLAGS_M32= -j2".
Next, after building klee-uclibc and get to step 6 configure KLEE, after
issuing the command
./configure --with-llvm=/nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9/
--with-stp=/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp/binary-build/
--with-uclibc=/nfs/adaptive/tnguyen/Src/Devel/KLEE/klee-uclibc/
--enable-posix-runtime,
I get the error about -lstp as below
checking for stp/c_interface.h... yes
checking for vc_setInterfaceFlags in -lstp... no
configure: error: Unable to link with libstp
As suggested from this msg
http://keeda.stanford.edu/pipermail/klee-dev/2012-October/000940.html , I
checked and verified the file lib/libstp.a etc are in the STP dir. The
command readelf -h lib/libstp.a gives something like
File: lib/libstp.a(SMTLIBPrinter.cpp.o)
ELF Header:
Class: ELF64
Data: 2's complement, little endian
Version: 1 (current)
Machine: Advanced Micro Devices X86-64
...
Note that I did build stp with CFLAGS_M32, i.e., make CFLAGS_M32= -j2.
I was able to build KLEE with STP r940 just fine on Debian so it seems
there's some incompatibility problem among Arch Linux, Klee, and STP. I
would appreciate any suggestion on how to get Klee built on my system.
Thanks in advance.
---
Arch system info: uname -a
Linux prime 3.11.6-1-ARCH #1 SMP PREEMPT Fri Oct 18 23:22:36 CEST 2013
x86_64 GNU/Linux
[1] error when building stp-r940
CVC.y:1109.3-1114.1: warning: rule useless in parser due to conflicts
[-Wother]
| Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
flex -Cfe -olexCVC.cpp -Pcvc CVC.lex
g++ -O2 -DCRYPTOMINISAT2 -I../../src/ -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated -c -o lexCVC.o lexCVC.cpp
g++ -O2 -DCRYPTOMINISAT2 -I../../src/ -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated -c -o parseCVC.o parseCVC.cpp
CVC.y: In function âint cvcparse()â:
CVC.y:211:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
^
CVC.y:217:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
^
CVC.y:233:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(asserts);
^
<builtin>: recipe for target 'parseCVC.o' failed
make[1]: *** [parseCVC.o] Error 1
make[1]: Leaving directory
'/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp-r940/src/parser'
Makefile:26: recipe for target 'all' failed
make: *** [all] Error 2
Vu,
I try to build Klee using the instruction from this page
http://ccadar.github.io/klee/GetStarted.html . I was not able to build
stp-r940.tgz, after doing "make OPTIMIZE=-O2 CFLAGS_M32= install" , I get
error about AssertsQuery not declared in scope (see [1]). So I try the
latest version of stp as suggested from this message
http://www.mail-archive.com/klee-dev-AQ/***@public.gmane.org/msg01315.html . I was
able to build this stp version fine with the make command "make
CFLAGS_M32= -j2".
Next, after building klee-uclibc and get to step 6 configure KLEE, after
issuing the command
./configure --with-llvm=/nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9/
--with-stp=/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp/binary-build/
--with-uclibc=/nfs/adaptive/tnguyen/Src/Devel/KLEE/klee-uclibc/
--enable-posix-runtime,
I get the error about -lstp as below
checking for stp/c_interface.h... yes
checking for vc_setInterfaceFlags in -lstp... no
configure: error: Unable to link with libstp
As suggested from this msg
http://keeda.stanford.edu/pipermail/klee-dev/2012-October/000940.html , I
checked and verified the file lib/libstp.a etc are in the STP dir. The
command readelf -h lib/libstp.a gives something like
File: lib/libstp.a(SMTLIBPrinter.cpp.o)
ELF Header:
Class: ELF64
Data: 2's complement, little endian
Version: 1 (current)
Machine: Advanced Micro Devices X86-64
...
Note that I did build stp with CFLAGS_M32, i.e., make CFLAGS_M32= -j2.
I was able to build KLEE with STP r940 just fine on Debian so it seems
there's some incompatibility problem among Arch Linux, Klee, and STP. I
would appreciate any suggestion on how to get Klee built on my system.
Thanks in advance.
---
Arch system info: uname -a
Linux prime 3.11.6-1-ARCH #1 SMP PREEMPT Fri Oct 18 23:22:36 CEST 2013
x86_64 GNU/Linux
[1] error when building stp-r940
CVC.y:1109.3-1114.1: warning: rule useless in parser due to conflicts
[-Wother]
| Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
flex -Cfe -olexCVC.cpp -Pcvc CVC.lex
g++ -O2 -DCRYPTOMINISAT2 -I../../src/ -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated -c -o lexCVC.o lexCVC.cpp
g++ -O2 -DCRYPTOMINISAT2 -I../../src/ -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated -c -o parseCVC.o parseCVC.cpp
CVC.y: In function âint cvcparse()â:
CVC.y:211:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
^
CVC.y:217:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
^
CVC.y:233:13: error: âAssertsQueryâ was not declared in this scope
((ASTVec*)AssertsQuery)->push_back(asserts);
^
<builtin>: recipe for target 'parseCVC.o' failed
make[1]: *** [parseCVC.o] Error 1
make[1]: Leaving directory
'/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp-r940/src/parser'
Makefile:26: recipe for target 'all' failed
make: *** [all] Error 2
Vu,