[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C. Compiling Maria


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C.1 System Requirements

Special care has been taken to ensure the quality and portability of the Maria source code. The code should compile on any ISO/IEC 14882 compliant C++ compiler. Unfortunately the standard is fairly new (summer 1998), and until 2001 or 2002, many C++ compilers did not support even the subset of it that compiling Maria requires.

We use the GNU Compiler Collection (gcc) on Debian GNU/Linux as the development platform. GCC should be able to compile the program also on FreeBSD, NetBSD, OpenBSD and IBM AIX systems. Furthermore, the code can be compiled with the native compilers of Digital UNIX 4.0 and 5.1, HP-UX 11.22, Sun Solaris 8, SGI IRIX 6.2 and Apple Darwin 5.3.

It is recommended that you install the freely available gcc 2.95 or later on your system if you have problems compiling the code.

We would like to hear success reports from people using other compilers. Patches, even to the ‘Makefile’ files, are welcome.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C.2 Editing the ‘Makefile’ files

In the top-level directory, in ‘Makefile’ and in ‘Makefile’.system, there are a couple of variable definitions that you should check before invoking the compilation by typing ‘make’. It is recommended to make ‘reallyclean’ before re-starting the compilation after making modifications.(7)

HAS_READLINE
LIBREADLINE
INCREADLINE

Set ‘HAS_READLINE=yes’ if the GNU Readline library is available, and ensure that the directories have been set up properly. The library is not a necessity; See section The Line Editor, for the features it provides. On some systems, you may need to add ‘-lncurses’ to the list of libraries.

EXPR_COMPILE

Set ‘EXPR_COMPILE=yes’ if your system supports dynamic loading of shared libraries and if you want to enable the ‘-C’ command line option (see section Options), which will considerably speed up the state space exploration.

EXTRA_DEFINES

Extra definitions for the macro preprocessor. Set ‘-DUSE_MMAP’ in order to enable memory mapped access to the reachability graph files on systems that implement the POSIX.1b mmap(2) interface. This option can considerably speed up the analysis of models that have a relatively small number of high-level transitions. Please note that with this option, 32-bit systems can only handle graph files whose total size is less than 4 gigabytes, maybe even less than 1 gigabyte, depending on the operating system.

DEBUG

Debugging flags. Usually ‘-DNDEBUG’ for compiling the production version and ‘-g’ for the debugging version.

PROF

Profiling flags. Usually empty.

CXX
CC

Commands for compiling modules written in C++ and C, respectively.

EXTRA_LIBS

Define ‘EXTRA_LIBS=-ldl’ or similar, if you want to enable support for compiled expressions and the dynamic loader routines are not part of the standard libraries on your system.

DEFINES

Extra flags e.g. for enabling the usage of the POSIX regular expression library (‘-DHAS_REGEX’), of the ‘getopt_long’ function (‘-DHAS_GETOPT_LONG’), a GNU extension to the standard, and of some extensions to the Standard Template Library (‘-DHASH_MAP_LOC’ and ‘-DSLIST_LOC’).

CFLAGS
CXXFLAGS

Flags for the C and C++ compilers e.g. for enabling optimizations.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C.3 Installing Maria

The file ‘Makefile’ in the top-level directory contains rules for installing the ‘maria’ executable and some related files on Unix-like systems. The installation is invoked by typing ‘make install installman installinfo’. You may want to redefine some of the following variables either in the ‘Makefile’ or on the ‘make’ command line:

PREFIX

The base directory where Maria should be installed. You might want to change this to ‘/usr/local’. The default is ‘/usr’.

INSTALLDIR
INSTALLBIN
INSTALLDATA

The commands for creating directories, installing executable files and installing data files. On Apple Darwin, you will need to add the ‘-c’ switch to the latter two commands.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C.4 Compiling Maria for Debugging

Compiling a debugging version of Maria is simple: in ‘Makefile’, define ‘DEBUG=-g’, and you are all set. You could also disable ‘assert()’ macros by defining ‘-DNDEBUG’, but they are very useful, since they often catch errors introduced by modifying code that seems completely unrelated to the failed assertion at first sight.

For detecting and debugging memory management issues, you can use the Electric Fence Library, Valgrind for GNU/Linux, the Debug Malloc Library (See (dmalloc)Top or http://www.dmalloc.com) or commercial tools such as Third Degree (‘third’) on Digital UNIX.

Debuggers often have problems with C++. For us, the GNU debugger (gdb 5.0) and has worked pretty well on Debian GNU/Linux. Version 4.18 has problems calling virtual methods.

Defining the ‘YYDEBUG’ macro enables grammar debugging. An executable compiled with this macro defined will look for the environment variable DEBUG. When DEBUG=1, the parser will print out more than enough information on the parsing process. Often it makes sense to set a conditional breakpoint on the lexical analyzer function based on the input line number, and to enable the parser debugging output only for a certain region of the input by setting or clearing the status variable in the debugger.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

C.5 Reporting Bugs

Every non-trivial program is likely to contain bugs. Fatal bugs, such as assertion failures or segmentation faults, are easiest to locate. Our intention has been to make the parsers in Maria bullet-proof: no matter what the input is, the program should not crash.

Sometimes a program may behave in a counter-intuitive way, doing something else than one would except. Such situations can be caused by a bug, or the program might behave just as planned. The latter case is often fixed by rephrasing or extending the documentation.

Bug reports and suggestions are welcome at ‘msmakela@tcs.hut.fi’. In the bug reports, please mention which platform you are using (including version numbers of the operating system and the relevant compilers and libraries) and include a stripped-down input file that is enough for triggering the bug. You can also compile the analyzer with support for debugging enabled, since it can help tracking down the error. Please use the ‘diff -c’ format for any patches you send.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by root on December 1, 2016 using texi2html 1.82.