configure: error: Could not find a version of the library!

156 views
Skip to first unread message

Siddharth Krishna

unread,
Feb 24, 2015, 11:34:27 PM2/24/15
to ufo-d...@googlegroups.com
Hi,

I was trying to compile UFO from source, following the instructions posted here:
and also using the script posted by Charlie Jacobsen here:

I managed to install all the dependencies, but got stuck after cloning the UFO repository and trying to run ./configure:

~/ufo-project/ufo-base$ ./configure --prefix=/home/siddharth/ufo-project/ufo-base-run --with-llvmsrc=/home/siddharth/ufo-project/llvm/src/llvm-2.9 --with-llvmobj=/home/siddharth/ufo-project/llvm/build/llvm-2.9 --with-msat=/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64 --with-llvmbin=/home/siddharth/ufo-project/llvm/run/llvm-2.9 --with-llvmgccbin=/home/siddharth/ufo-project/llvm/run/llvm-gcc4.2-2.9-x86_64-linux --with-z3=/home/siddharth/ufo-project/z3/run/z3 --with-ldd=/home/siddharth/ufo-project/ldd/run/ldd-r6438 --with-apron=/home/siddharth/ufo-project/apron/run/trunk
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking how to run the C++ preprocessor... g++ -E
checking for grep that handles long lines and -e... /bin/grep
checking for egrep... /bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking size of void *... 8
checking size of long... 8
checking size of int... 4
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking target system type... x86_64-unknown-linux-gnu
checking for boostlib >= 1.46.1... yes
checking for gcc... gcc
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking whether the Boost::System library is available... yes
configure: error: Could not find a version of the library!
~/ufo-project/ufo-base$ 

I'm running ubuntu 14.04, and used the first version of Charlie's script, because I didn't want to install another version of gcc/g++. Any idea what library the configure script could not find? Its not the boost library, because I installed that via apt-get...

Thanks in advance!

Siddharth

Arie Gurfinkel

unread,
Feb 24, 2015, 11:40:46 PM2/24/15
to ufo-d...@googlegroups.com, Siddharth Krishna
Hey, the configure build system is old and is not supported by the current development version of UFO.

Please follow the cmake-based build instructions from here: https://bitbucket.org/arieg/ufo/src/258efef796e4384dcb45f6ce24168a37cdfc02c1/?at=develop

Note that this requires that LLVM is compiled using cmake as well. 
You can use the old instructions to compile the dependencies. 

cheers,
arie

--
You received this message because you are subscribed to the Google Groups "UFO General Discussion Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ufo-discuss...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Siddharth Krishna

unread,
Feb 25, 2015, 12:35:48 AM2/25/15
to Arie Gurfinkel, ufo-d...@googlegroups.com
Hi,

Oh, I see, thanks a lot. I just tried again with cmake, managed to compile llvm, and configure the ufo build, but make ufo threw some errors. I checked to make sure it was the latest source (tried master and develop branches). I hope I'm not missing something silly:

~/ufo-project/build$ make ufo
[  3%] Building CXX object lib/Cpg/CMakeFiles/UFOCpg.dir/Lbe.cpp.o
[  6%] Building CXX object lib/Cpg/CMakeFiles/UFOCpg.dir/Topo.cpp.o
[ 10%] Building CXX object lib/Cpg/CMakeFiles/UFOCpg.dir/Wto.cpp.o
Linking CXX static library libUFOCpg.a
[ 10%] Built target UFOCpg
[ 13%] Building CXX object lib/Asd/Bnd/CMakeFiles/UFOBnd.dir/BoundAbstractStateDomain.cpp.o
In file included from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:8:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/VarBound.hpp:12,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/BoundAbstractStateDomain.hpp:10,
                 from /home/siddharth/ufo-project/ufo-base/lib/Asd/Bnd/BoundAbstractStateDomain.cpp:1:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp: In member function ‘_Z3_config* ufoz3::Z3<T, EC>::mkConfig()’:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:124:62: error: there are no arguments to ‘Z3_global_param_set’ that depend on a template parameter, so a declaration of ‘Z3_global_param_set’ must be available [-fpermissive]
    Z3_global_param_set (kv.first.c_str (), kv.second.c_str ());
                                                              ^
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:124:62: note: (if you use ‘-fpermissive’, G++ will accept your code, but allowing the use of an undeclared name is deprecated)
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp: In member function ‘void ufoz3::Z3<T, EC>::startLogging(std::string)’:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:163:33: error: cannot convert ‘const char*’ to ‘Z3_context {aka _Z3_context*}’ for argument ‘1’ to ‘Z3_bool Z3_open_log(Z3_context, Z3_string)’
       Z3_open_log (fname.c_str());
                                 ^
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp: In member function ‘void ufoz3::Z3<T, EC>::stopLogging()’:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:169:21: error: too few arguments to function ‘void Z3_close_log(Z3_context)’
       Z3_close_log ();
                     ^
In file included from /home/siddharth/ufo-project/z3/run/z3/include/z3.h:67:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:5,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:8,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/VarBound.hpp:12,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/BoundAbstractStateDomain.hpp:10,
                 from /home/siddharth/ufo-project/ufo-base/lib/Asd/Bnd/BoundAbstractStateDomain.cpp:1:
/home/siddharth/ufo-project/z3/run/z3/include/z3_api.h:3998:17: note: declared here
     void Z3_API Z3_close_log(__in Z3_context c);
                 ^
In file included from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:8:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/VarBound.hpp:12,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/BoundAbstractStateDomain.hpp:10,
                 from /home/siddharth/ufo-project/ufo-base/lib/Asd/Bnd/BoundAbstractStateDomain.cpp:1:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp: In instantiation of ‘void ufoz3::Z3<T, EC>::init() [with T = boost::intrusive_ptr<expr::ENode>; EC = ufo::z3::BasicExprConverter<ufo::z3::TerminalUfo<ufo::z3::TerminalAssert> >]’:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:71:13:   required from ‘ufoz3::Z3<T, EC>::Z3(expr::ExprFactory&, const StringMap&, bool) [with T = boost::intrusive_ptr<expr::ENode>; EC = ufo::z3::BasicExprConverter<ufo::z3::TerminalUfo<ufo::z3::TerminalAssert> >; ufo::StringMap = std::map<std::basic_string<char>, std::basic_string<char> >]’
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:748:31:   required from here
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:151:47: error: invalid conversion from ‘void (*)(Z3_context, Z3_error_code) {aka void (*)(_Z3_context*, Z3_error_code)}’ to ‘void (*)(Z3_error_code)’ [-fpermissive]
       Z3_set_error_handler (ctx, error_handler);
                                               ^
In file included from /home/siddharth/ufo-project/z3/run/z3/include/z3.h:67:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:5,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:8,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/VarBound.hpp:12,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/BoundAbstractStateDomain.hpp:10,
                 from /home/siddharth/ufo-project/ufo-base/lib/Asd/Bnd/BoundAbstractStateDomain.cpp:1:
/home/siddharth/ufo-project/z3/run/z3/include/z3_api.h:4298:17: error:   initializing argument 2 of ‘void Z3_set_error_handler(Z3_context, void (*)(Z3_error_code))’ [-fpermissive]
     void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h);
                 ^
In file included from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:8:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/VarBound.hpp:12,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Asd/Bnd/BoundAbstractStateDomain.hpp:10,
                 from /home/siddharth/ufo-project/ufo-base/lib/Asd/Bnd/BoundAbstractStateDomain.cpp:1:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp: In instantiation of ‘_Z3_config* ufoz3::Z3<T, EC>::mkConfig() [with T = boost::intrusive_ptr<expr::ENode>; EC = ufo::z3::BasicExprConverter<ufo::z3::TerminalUfo<ufo::z3::TerminalAssert> >; Z3_config = _Z3_config*]’:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:148:34:   required from ‘void ufoz3::Z3<T, EC>::init() [with T = boost::intrusive_ptr<expr::ENode>; EC = ufo::z3::BasicExprConverter<ufo::z3::TerminalUfo<ufo::z3::TerminalAssert> >]’
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:71:13:   required from ‘ufoz3::Z3<T, EC>::Z3(expr::ExprFactory&, const StringMap&, bool) [with T = boost::intrusive_ptr<expr::ENode>; EC = ufo::z3::BasicExprConverter<ufo::z3::TerminalUfo<ufo::z3::TerminalAssert> >; ufo::StringMap = std::map<std::basic_string<char>, std::basic_string<char> >]’
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ExprZ3.hpp:748:31:   required from here
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3.hpp:124:62: error: ‘Z3_global_param_set’ was not declared in this scope
    Z3_global_param_set (kv.first.c_str (), kv.second.c_str ());
                                                              ^
make[3]: *** [lib/Asd/Bnd/CMakeFiles/UFOBnd.dir/BoundAbstractStateDomain.cpp.o] Error 1
make[2]: *** [lib/Asd/Bnd/CMakeFiles/UFOBnd.dir/all] Error 2
make[1]: *** [tools/ufo/CMakeFiles/ufo.dir/rule] Error 2
make: *** [ufo] Error 2
~/ufo-project/build$


Is this some C++ version mismatch?

Thanks,


Siddharth

Arie Gurfinkel

unread,
Feb 25, 2015, 8:25:54 AM2/25/15
to Siddharth Krishna, ufo-d...@googlegroups.com
You are either using a wrong version of Z3 or wrong header files. 
Check that z3_api.h declares Z3_global_param_set() function.

I expect UFO to compile against the unstable branch of the main z3 repo on codeplex. 


If you are still having problems, send me the output of 

make VERBOSE=1

cheers,
arie



Siddharth Krishna

unread,
Feb 25, 2015, 9:09:29 AM2/25/15
to Arie Gurfinkel, ufo-discuss
Which version of Z3 am I supposed to use? I was using 3.2 as advised by the Installation Instructions page.

Here is the output of make VERBOSE=1. I guess you're right, it can't find z3++.h, which doesn't seem to be in the z3 distribution linked on the Installation Instructions page..

~/ufo-project/build$ make VERBOSE=1
/usr/bin/cmake -H/home/siddharth/ufo-project/ufo-base -B/home/siddharth/ufo-project/build --check-build-system CMakeFiles/Makefile.cmake 0
/usr/bin/cmake -E cmake_progress_start /home/siddharth/ufo-project/build/CMakeFiles /home/siddharth/ufo-project/build/CMakeFiles/progress.marks
make -f CMakeFiles/Makefile2 all
make[1]: Entering directory `/home/siddharth/ufo-project/build'
make -f lib/Util/CMakeFiles/UFOUtil.dir/build.make lib/Util/CMakeFiles/UFOUtil.dir/depend
make[2]: Entering directory `/home/siddharth/ufo-project/build'
cd /home/siddharth/ufo-project/build && /usr/bin/cmake -E cmake_depends "Unix Makefiles" /home/siddharth/ufo-project/ufo-base /home/siddharth/ufo-project/ufo-base/lib/Util /home/siddharth/ufo-project/build /home/siddharth/ufo-project/build/lib/Util /home/siddharth/ufo-project/build/lib/Util/CMakeFiles/UFOUtil.dir/DependInfo.cmake --color=
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
make -f lib/Util/CMakeFiles/UFOUtil.dir/build.make lib/Util/CMakeFiles/UFOUtil.dir/build
make[2]: Entering directory `/home/siddharth/ufo-project/build'
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 18
[  3%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/AlwaysInlineMark.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/AlwaysInlineMark.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/AlwaysInlineMark.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 19
[  6%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/ErrorExit.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/ErrorExit.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/ErrorExit.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 20
[  9%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/ExitReturn.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/ExitReturn.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/ExitReturn.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 21
[ 12%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/NameValues.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/NameValues.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/NameValues.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 22
[ 16%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/NondetInit.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/NondetInit.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/NondetInit.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 23
[ 19%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/ReturnGoto.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/ReturnGoto.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/ReturnGoto.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 24
[ 22%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/ShadowMem.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/ShadowMem.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/ShadowMem.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 25
[ 25%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/Stats.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/Stats.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/Stats.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 26
[ 29%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/UfoDebug.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/UfoDebug.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/UfoDebug.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 27
[ 32%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/SetLimitsOpts.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/SetLimitsOpts.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/SetLimitsOpts.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 28
[ 35%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/ufocl.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/ufocl.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/ufocl.cpp
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 29
[ 38%] Building CXX object lib/Util/CMakeFiles/UFOUtil.dir/EdgeComp.cpp.o
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOUtil.dir/EdgeComp.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Util/EdgeComp.cpp
Linking CXX static library libUFOUtil.a
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/cmake -P CMakeFiles/UFOUtil.dir/cmake_clean_target.cmake
cd /home/siddharth/ufo-project/build/lib/Util && /usr/bin/cmake -E cmake_link_script CMakeFiles/UFOUtil.dir/link.txt --verbose=1
/usr/bin/ar cr libUFOUtil.a  CMakeFiles/UFOUtil.dir/AlwaysInlineMark.cpp.o CMakeFiles/UFOUtil.dir/ErrorExit.cpp.o CMakeFiles/UFOUtil.dir/ExitReturn.cpp.o CMakeFiles/UFOUtil.dir/NameValues.cpp.o CMakeFiles/UFOUtil.dir/NondetInit.cpp.o CMakeFiles/UFOUtil.dir/ReturnGoto.cpp.o CMakeFiles/UFOUtil.dir/ShadowMem.cpp.o CMakeFiles/UFOUtil.dir/Stats.cpp.o CMakeFiles/UFOUtil.dir/UfoDebug.cpp.o CMakeFiles/UFOUtil.dir/SetLimitsOpts.cpp.o CMakeFiles/UFOUtil.dir/ufocl.cpp.o CMakeFiles/UFOUtil.dir/EdgeComp.cpp.o
/usr/bin/ranlib libUFOUtil.a
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles  18 19 20 21 22 23 24 25 26 27 28 29
[ 38%] Built target UFOUtil
make -f lib/Cpg/CMakeFiles/UFOCpg.dir/build.make lib/Cpg/CMakeFiles/UFOCpg.dir/depend
make[2]: Entering directory `/home/siddharth/ufo-project/build'
cd /home/siddharth/ufo-project/build && /usr/bin/cmake -E cmake_depends "Unix Makefiles" /home/siddharth/ufo-project/ufo-base /home/siddharth/ufo-project/ufo-base/lib/Cpg /home/siddharth/ufo-project/build /home/siddharth/ufo-project/build/lib/Cpg /home/siddharth/ufo-project/build/lib/Cpg/CMakeFiles/UFOCpg.dir/DependInfo.cmake --color=
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
make -f lib/Cpg/CMakeFiles/UFOCpg.dir/build.make lib/Cpg/CMakeFiles/UFOCpg.dir/build
make[2]: Entering directory `/home/siddharth/ufo-project/build'
make[2]: Nothing to be done for `lib/Cpg/CMakeFiles/UFOCpg.dir/build'.
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles  12 13 14
[ 48%] Built target UFOCpg
make -f lib/Horn/CMakeFiles/UFOHorn.dir/build.make lib/Horn/CMakeFiles/UFOHorn.dir/depend
make[2]: Entering directory `/home/siddharth/ufo-project/build'
cd /home/siddharth/ufo-project/build && /usr/bin/cmake -E cmake_depends "Unix Makefiles" /home/siddharth/ufo-project/ufo-base /home/siddharth/ufo-project/ufo-base/lib/Horn /home/siddharth/ufo-project/build /home/siddharth/ufo-project/build/lib/Horn /home/siddharth/ufo-project/build/lib/Horn/CMakeFiles/UFOHorn.dir/DependInfo.cmake --color=
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
make -f lib/Horn/CMakeFiles/UFOHorn.dir/build.make lib/Horn/CMakeFiles/UFOHorn.dir/build
make[2]: Entering directory `/home/siddharth/ufo-project/build'
/usr/bin/cmake -E cmake_progress_report /home/siddharth/ufo-project/build/CMakeFiles 15
[ 51%] Building CXX object lib/Horn/CMakeFiles/UFOHorn.dir/HornMain.cpp.o
cd /home/siddharth/ufo-project/build/lib/Horn && /usr/bin/c++    -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include   -D_GNU_SOURCE   -Wno-unused-parameter -Wwrite-strings  -Wno-long-long -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS -fopenmp -DBSD -DHAVE_IEEE_754 -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 -g -I/home/siddharth/ufo-project/llvm/run/llvm-2.9/include -I/usr/include/x86_64-linux-gnu -I/home/siddharth/ufo-project/mathsat/run/mathsat-5.2.6-linux-x86_64/include -I/home/siddharth/ufo-project/z3/run/z3/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/src/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/include -I/home/siddharth/ufo-project/ldd/run/ldd-r6438/cudd-2.4.2/cudd -I/home/siddharth/ufo-project/apron/run/trunk/include -I/home/siddharth/ufo-project/ufo-base/include -I/home/siddharth/ufo-project/build/include    -o CMakeFiles/UFOHorn.dir/HornMain.cpp.o -c /home/siddharth/ufo-project/ufo-base/lib/Horn/HornMain.cpp
In file included from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/ZExprConverter.hpp:8:0,
                 from /home/siddharth/ufo-project/ufo-base/include/ufo/Smt/UfoZ3.hpp:5,
                 from /home/siddharth/ufo-project/ufo-base/lib/Horn/HornMain.cpp:12:
/home/siddharth/ufo-project/ufo-base/include/ufo/Smt/Z3n.hpp:15:18: fatal error: z3++.h: No such file or directory
 #include "z3++.h"
                  ^
compilation terminated.
make[2]: *** [lib/Horn/CMakeFiles/UFOHorn.dir/HornMain.cpp.o] Error 1
make[2]: Leaving directory `/home/siddharth/ufo-project/build'
make[1]: *** [lib/Horn/CMakeFiles/UFOHorn.dir/all] Error 2
make[1]: Leaving directory `/home/siddharth/ufo-project/build'
make: *** [all] Error 2


~/ufo-project/build$ ls ../z3/run/z3/bin
z3
~/ufo-project/build$ ls ../z3/run/z3/include
z3_api.h  z3.h
~/ufo-project/build$ ls ../z3/run/z3/lib
libz3.a  libz3.so



Siddharth

Arie Gurfinkel

unread,
Feb 25, 2015, 9:26:13 AM2/25/15
to Siddharth Krishna, ufo-discuss
Sorry. The instructions there are old. Please use either spacer branch or unstable branch of the current z3 distribution. 

See my prev email for details. 

cheers
arie


--
On the move ...

Siddharth Krishna

unread,
Feb 25, 2015, 3:57:42 PM2/25/15
to Arie Gurfinkel, ufo-discuss
Hi,

Thanks for all the help. I managed to get everything to compile! :) (haven't tried the front end yet).

I'm listing things I did differently from the instructions here in case it's useful to someone else:

1. I had to additionally install the packages libboost-dev-all, and libreadline-dev.

2. I had to copy some files from the llvm build directory to the install directory (this wasn't an error but a warning).

I've attached the script I used, for reference.

Best,

Siddharth
ufo-build.sh

Arie Gurfinkel

unread,
Feb 25, 2015, 4:38:06 PM2/25/15
to Siddharth Krishna, ufo-discuss
Great! For the front-end, you might get away with using the binary only.

cheers,
arie
Reply all
Reply to author
Forward
0 new messages