forked from hotelzululima/insight
-
Notifications
You must be signed in to change notification settings - Fork 1
/
INSTALL
193 lines (139 loc) · 6.3 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
Insight Installation Instructions
===================================
Table of contents:
1 - Basic Build and Install
2 - MacOS X Build and Install
3 - Building in a separate directory
4 - Installing external SMT solvers
5 - Using more binutils file formats/architectures
6 - Developer Build and Install
7 - Generate the Doxygen documentation
8 - Test Framework (ATF/Kyua)
-----------------------------------
1 - Basic Build and Install
===========================
The insight framework needs a UNIX-like environment to build and work
properly. It relies on a small number of widely used libraries and
tools, and here is the list of dependencies if you downloaded the
tarball of a release. Package names may vary depending on your
operating system distribution.
binutils
g++
libstl (probably provided with g++)
libxml2
Insight can be easily installed thanks to the usual:
'./configure && make && make install'.
In case of error, the 'configure' script should provide some useful
error messages that will help you to get through.
2 - MacOS X Build and Install
============================
Under MacOS X, you will need to install UNIX packages either by hand
or by using MacPorts, Fink, or similar package systems. We tested and
use insight with MacPorts (http://www.macports.org/).
The insight framework needs the following additional packages to build
and operate:
Apple's XCode
binutils
libxml2
pkgconfig
./configure CPPFLAGS=-I/opt/local/include \
LDFLAGS=-L/opt/local/lib/x86_64
Note that, if you are using a system older than Snow Leopard (10.6.x),
you will need to use a slightly different command line:
./configure CPPFLAGS=-I/opt/local/include \
LDFLAGS=-L/opt/local/lib
The paths given are correct for MacPorts. Fink uses /sw as its root
directory.
Possibly unusual configure flags are available:
--enable-werror compile with -Werror flag (default is no)
--enable-debug compile with debug (default is no)
--enable-optimization compile with optimization (default is no)
3 - Building in a separate directory
====================================
If you want to build the project outside of the source directory, just
create a fresh directory (eg. 'build/'), cd into it and type:
<path_to_srcdir>/configure <suitable_options>
This should run exactly as if you were in the source directory but
keeping built files apart from the source files.
We recommend this way of building as it leaves the source directory
clean.
4 - Installing external SMT solvers (Z3/MathSAT 5)
==================================================
Some algorithms require calls to a SMT Solver. The current implementation
uses the solver as a separate process and requests/responses are sent through
pipes. This design makes Insight relatively independant from the installed
solver; however only Z3 4.3.2 (or higher) and MathSAT 5.2.6 have been tested.
You can get them at the following URLs:
- MathSAT 5
* Project : http://mathsat.fbk.eu/
* Download: http://mathsat.fbk.eu/download.html
- Z3
* Project : http://research.microsoft.com/en-us/um/redmond/projects/z3/
* Source code: http://z3.codeplex.com/
5 - Using more binutils file formats/architectures
==================================================
On most operating system distributions the binutils package comes only
with the minimum needed processor architectures and binary formats. In
fact, the binutils can do much more than that and can deal with a lot
of architectures and binary formats.
The Debian-based systems propose a binutils-multiarch package that
includes among others ARM support and adds several extra binary
formats. It is generally a good idea to install it and to execute the
following command as root (we assume binutils-x.xx):
# cd /usr/lib/
# ln -s libbfd-x.xx-multiarch.so libbfd-multiarch.so
# ln -s libopcodes-x.xx-multiarch.so libopcodes-multiarch.so
If you do not have a Debian-based system, or if you want more than
what binutils-multiarch package provides, you will need to recompile
and install the binutils by yourself.
Getting the sources can be done by FTP:
ftp://ftp.gnu.org/gnu/binutils/
Building the sources goes as usual, except that we will ask configure
to build all the binutils supported targets this way:
./configure --enable-targets=all && make && make install
Under NetBSD, we found it necessary to pass also the '--disable-nls'
option to configure.
Under Linux, you will have to pass the '--enable-shared' option to
configure.
You will probably need to point to this installation of the binutils
when invoking 'configure' within insight. E.g.:
./configure CPPFLAGS=-I/usr/local/include LDFLAGS=-L/usr/local/lib
6 - Developer Build and Install
===============================
Developers are, of course, more than welcome in this project and
feature requests, development questions and patches will be looked at
and commented upon by the Insight team (see the README file for more
contact information).
In order to build insight from a fresh checkout of the sources, you
will need the following additional packages:
autoconf
automake
bison (/usr/bin/bison is too old under MacOS X)
flex
GNU libtool
Getting a fresh development snapshot of the source:
$ svn checkout https://insight.labri.fr/svn/trunk insight
Then, change to the directory you just checked out ('insight' here)
and you will be able to generate all the autoconf stuff with:
./autogen.sh
You can then proceed with the usual 'configure' step.
7 - Generate the Doxygen documentation
======================================
Insight comes with a Doxygen API documentation. We chose to not build
it by default to spare time and space. Yet, building the HTML API
documentation can be done as follow (in the following we assume that
the build is in the 'build' directory):
1) Go to build/doc
2) Type: make api
3) Documentation will appear in build/doc/api/html/
8 - Test Framework (ATF/Kyua)
=============================
We use the ATF/Kyua test framework runner in order to test insight. At
the moment, Kyua is not available as a package on most systems. So,
the best way to go is to install it directly from their stable or
development sources. First install ATF, then install the kyua-cli
application.
ATF Project: git clone https://github.com/jmmv/atf.git
Lutok Project: git clone https://github.com/jmmv/lutok.git
Kyua Project: git clone https://github.com/jmmv/kyua.git
Blog: http://julipedia.meroh.net/