HACKING 12.5 KB
Newer Older
1
2
Bootstraping from GIT
=====================
3
4
5

Some files in SPOT's source tree are generated.  They are distributed
so that users do not need to tools to rebuild them, but we don't keep
6
all of them under GIT because it can generate lots of changes or
7
8
conflicts.

9
Here are the tools you need to bootstrap the GIT tree, or more
10
generally if you plan to regenerate some of the generated files.
11
12
(None of these tools are required by end users installing a tarball
since the generated files they produce are distributed.)
13

14
  GNU Autoconf >= 2.61
15
  GNU Automake >= 1.11
16
  GNU Libtool >= 2.4
17
18
  GNU Flex (the version seems to matters, we used 2.5.35)
  GNU Bison >= 2.4.2
19
  GNU Emacs (preferably >= 24 but it may work with older versions)
20
  SWIG >= 1.3.31
21
  Doxygen >= 1.4.0
22
23
24
  Perl, with its Gettext module (it might be called something like
    liblocale-gettext-perl or p5-locale-gettext in your distribution)
  A complete LaTeX distribution, including latexmk.
25

26
Bootstrap the GIT tree by running
27

28
  % autoreconf -vfi
29

30
and then go on with the usual
31

32
33
  % ./configure
  % make
34

35

36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
Tricks
======

Avoiding Doxygen runs
---------------------

When there is no documentation built (e.g., after a fresh checkout
of the GIT tree), when the configure.ac file has changed, or when
the Doxygen configuration has changed, the doc will be rebuilt.

This can take quite some time, even though recent version of Doxygen
have started to parallelize things.  If you have no interest
in generating the documentation, just use the "magic touch":

  touch doc/stamp

Do that right before running make.  The timestamp of doc/stamp
is compared to configure.ac and Doxygen.in to decide if the
documentation is out-of-date.  The above command pretends the
documentation has just been built.


58
59
60
61
62
63
64
65
66
67
68
69
Avoiding org-mode runs
----------------------

The files in doc/org/ are org-mode files (a mode of Emacs that we use
to author documents that embed executable snippets), they are used to
generate the doc/userdoc/ HTML documentation.  If for some reason you
don't have emacs, or you simply want not to rebuild these files, use
another "magic touch":

  touch doc/org-stamp


70
71
72
Debugging Libtool executables
-----------------------------

73
The executables generated in the various testsuite directories of Spot
74
are not real binaries.  Because we use libtool to compile the spot
75
76
library in a portable manner, these executables are just scripts that
run the actual binary after setting some environment variables so that
77
78
the OS can find the library in the build tree.

79
80
A consequence is that tools like gdb or valgrind, that expect to work
on a binary, will be confused by the script.  Example:
81
82
83
84
85
86
87
88

  % cd src/tgbatest
  % file ltl2tgba
  ltl2tgba: POSIX shell script text executable
  % gdb -q ltl2tgba
  "/home/adl/git/spot/src/tgbatest/ltl2tgba": not in executable format: File format not recognized
  (gdb) quit

89
90
The proper way to run any command on these fake binaries is via
libtool:
91
92
93
94
95
96
97

  % ../../libtool --mode=execute file ltl2tgba
  /home/adl/git/spot/src/tgbatest/.libs/lt-ltl2tgba: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.18, not stripped
  % ../../libtool --mode=execute gdb -q ltl2tgba
  Reading symbols from /home/adl/git/spot/src/tgbatest/.libs/lt-ltl2tgba...done.
  (gdb) quit

98
99
100
101
102
You can see that libtool turns ltl2tgba into .libs/lt-ltl2tgba, but it
also sets environment variables so that the dependent shared libraries
will be found.

If you are building Spot from the GIT repository, the libtool script
103
104
105
106
generated the root of the build tree should be the same as the libtool
script that is installed on your system.  So you can simply run
libtool instead of ../../libtool.

107
There is an undocumented feature of libtool that allows you to
108
shorthand "libtool --mode=execute" as "libtool execute" or even
109
110
111
112
113
114
115
116
"libtool e".  But you might also find convenient to define an alias, a
function, or a script to make that invocation even shorter.
For instance:

  alias le='libtool --mode=execute '

(The trailing space makes it possible to follow this command by
another aliased command.)
117
118


119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
Profiling with callgrind
------------------------

Install valgrind and kcachegrind.

Then run the command you want to profile through valgrind's callgrind
tool.  For instance:

  % libtool e valgrind --tool=callgrind ltl2tgba -f 'GFa & GFb'

This will output a file called 'callgrind.PID' where PID is the
process ID printed during valgrind's run.  Load this file with
kcachegrind to get a graphical summary.

  % kcachegrind ./callgrind.PID


136
137
138
139
140
Running coverage tests
----------------------

First, compile (and link) Spot with coverage enabled.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
141
  % ./configure CXX='g++ --coverage'
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
  % make

Then run the test suite (or any program you want to study).

  % make check

Executing programs using Spot will generate a lot of *.gc* files
everywhere.  Collect these using lcov:

  % lcov --capture --directory src --output spot.info

Finally generate a coverage report in HTML:

  % genhtml --legend --demangle-cpp --output-directory html spot.info

This should create the directory html/.


160
161
162
163
164
165
166
Link-time optimizations
-----------------------

This is currently (April 2011) tricky to setup, because the
toolchain is not mature enough.

You need:
167
168
169
170
171
172
  1. a version of GCC (>= 4.5) with gold and pluing linker enabled.
  2. a version of Libtool that knows how to deal with
     -flto flags (Libtool 2.4 will not work -- currently only
     the development version does.)
  3. to use static libraries instead of shared libraries
     so that you get inter-libraries optimizations.
173
174
175

Here are example options to pass to configure:

176
177
178
179
  ./configure CC=gcc-4.6 CXX=g++-4.6 \
              --disable-devel --disable-debug \
              CFLAGS='-flto' CXXFLAGS='-flto' LDFLAGS='-fuse-linker-plugin' \
              --disable-shared --enable-static
180

181
Using --disable-debug prevents the -g flag to be passed to the
182
183
184
185
186
187
188
compiler, which seems to help avoiding some internal compiler errors.

Some binaries (like ltl2tgba) currently fail to compile (internal
compiler error), while most others (like randtgba, dve2check, randltl,
...) do fine.


189
190
Coding conventions
==================
191
192

Here are the conventions we follow in Spot, so that the code looks
193
194
195
196
197
198
homogeneous.  Please follow these strictly.  Since this is free
software, uniformity of the code matters a lot.  Most of these
conventions are derived from the GNU Coding Standards
(http://www.gnu.org/prep/standards.html) with the notable exception
that we do not put a space before the opening parenthesis in function
calls (this is hardly readable when chaining method calls).
199

200
201
202
203
204
205
206
207

Encoding
--------

  * Use UTF-8 for non-ASCII characters.

  * If you edit files encoded in Latin-1 (the original default
    encoding for the project), feel free to convert them to UTF-8.
208
209
    In emacs the simplest way to convert the file is to add a comment
    with -*- coding: utf-8 -*- at the top or bottom of the file.
210

211
212
213
214
215
216
217
218
219
Comments
--------

  * The language to use is American.

  * When comments are sentences, they should start with a capital and
    end with a dot.  Dots that end sentences should be followed by two
    spaces (i.e., American typing convention), like in this paragraph.

220
221
222
  * Prefer C++-style comments (// foo) to C-style comments (/* foo */).
    Use /// for Doxygen comments.

223
224
225
Formating
---------

226
  * Braces are always on their own line.
227
228
229
230
231

  * Text within braces is two-space indented.

    {
      f(12);
232

233
234
235
236
237
238
239
240
241
242
243
244
    }

  * Anything after a control statement is two-space indented.  This
    includes braces.

    if (test)
      {
        f(123);
	while (test2)
	  g(456);
      }

245
  * Braces from function/structure/enum/class/namespace definitions
246
247
248
249
250
251
252
253
254
255
256
    are not indented.

    class foo
    {
    public:
      Foo();
    protected:
      static int get_mumble();
    };

  * The above corresponds to the `gnu' indentation style under Emacs.
257
258
259

  * Put return types and linkage specifiers on their own line in
    function/method _definitions_:
260
261
262
263
264
265
266
267
268

    static int
    Foo::get_mumble()
    {
      return 2;
    }

    This makes it easier to grep functions in the code.

269
270
271
    Function/method declaration are usually written on one line:

    int get_bar(int i);
272

273
  * Put a space before the opening parenthesis in control statements
274
275
276
277
278
279
280
281
282
283
284
285

    if (test)
      {
        do
	  {
	    something();
	  }
	while (0);
      }

  * No space before parentheses in function calls.
    (`some()->foo()->bar()' is far more readable than
286
    `some ()->foo ()->bar ()')
287
288
289

  * No space after opening or before closing parentheses, however
    put a space after commas (as in english).
290

291
    func(arg1, arg2, arg3);
292

293
294
295
296
297
298
299
300
301
  * No useless parentheses in return statements.

    return 2;    (not `return (2);')

  * Spaces around infix binary or ternary operators:

    2 + 2;
    a = b;
    a <<= (3 + 5) * 3 + f(67 + (really ? 45 : 0));
302

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
303
304
  * No space after prefix unary operators, or before postfix unary
    operators:
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320

    if (!test && y++ != 0)
      {
        ++x;
      }

  * When an expression spans over several lines, split it before
    operators.  If it's inside a parenthesis, the following lines
    should be 1-indented w.r.t. the opening parenthesis.

    if (foo_this_is_long && bar > win(x, y, z)
        && !remaining_condition)
      {
        ...
      }

321
322
  * `else if' can be put as-is on a single line.

323
324
  * No line should be larger than 80 columns.
    If a line takes more than 80 columns, split it or rethink it.
325

326
327
328
329
330
331
332
333
334
    This makes it easier to print the code, allow people to work on
    small screens, makes it possible to display two files (or an
    editor and a terminal) side-by-side, ...

    This also puts some pressure on the programmer who writes code
    that has too much nested blocks: if you find yourself having to
    code between columns 60 and 80 because of identation, consider
    writing helper functions to simplify the structure of your code.

335
  * Labels or case statements are back-indented by two spaces,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
336
    without space before the `:'.
337

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
    if (something)
      {
      top:
        bar = foo();
        switch (something_else)
	  {
	  case first_case:
	    f();
	    break;
	  case second_case:
	    g();
	    break;
	  default:
	    goto top;
	  }
      }

355
356
357
358
359
360
361
362
363
364
365
366
367
  * Pointers and references are part of the type, and should be put
    near the type, not near the variable.

      int* p;        // not `int *p;'
      list& l;       // not `list &l;'
      void* magic(); // not `void *magic();'

  * Do not declare many variables on one line.
    Use
      int* p;
      int* q;
    instead of
      int *p, *q;
368
    The former declarations also allow you to comment each variable.
369
370
371
372

  * The include guard for src/somedir/foo.hh is
    SPOT_SOMEDIR_FOO_HH

373
Naming
374
------
375
376
377
378
379
380
381

  * Functions, methods, types, classes, etc. are named with lowercase
    letters, using an underscore to separate words.

      int compute_this_and_that();

      class this_is_a_class;
382

383
384
385
386
      typedef int int_array[];

    That is the style used in STL.

387
  * Private members end with an underscore.
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408

    class my_class
    {
    public:
      ...
      int get_val() const;
    private:
      int name_;
    };

  * Identifiers (even internal) starting with `_' are best avoided
    to limit clashes with system definitions.

  * Template arguments use capitalized name, with joined words.

    template <class T, int NumberOfThings>
    class foo
    {
      ...
    };

409
  * Enum members also use capitalized name, with joined words.
410
411
412

  * C Macros are all uppercase.

413
414
  * Use *.hxx for the implementation of templates that are private to
    Spot (i.e., not installed) and need to be included multiple times.
415

416
Other style recommandations
417
---------------------------
418

419
420
  * Do not use the NULL macro, it is not always implemented in a way
    which is compatible with all pointer types.  Always use 0 instead.
421

422
423
424
425
426
  * Limit the scope of local variables by defining them as late as
    possible.  Do not reuse a local variables for two different things.

  * Do not systematically initialise local variables with 0 or other
    meaningless values.  This hides errors to valgrind.
427
428
429
430
431

  * Avoid <iostream>, <ostream>, etc. in headers whenever possible.
    Prefer <iosfwd> when predeclarations are sufficient, and then
    use for instance use just <ostream> in the corresponding .cc file.
    (A plain <iostream> is needed when using std::cout, std::cerr, etc.)
432
433
434
435
436
437

  * Always declare helper functions and other local class definitions
    (used in a single .cc files) in anonymous namespaces.  (The risk
    otherwise is to declare two classes with the same name: the linker
    will ignore one of the two silently.  The resulting bugs are often
    difficult to understand.)
438
439
440

  * Always code as if the person who ends up maintaining your code is
    a violent psychopath who knows where you live.