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

2. Installing Daikon

Shortcut for the impatient: skip directly to installation instructions (see section Unix/Linux/MacOS installation) (see section Windows installation).

There are two main ways to install Daikon. See section Simple installation instructions, for a simple 2-step installation process that is adequate for the needs of many users. See section Complete installation instructions, for a complete installation, in 4 easy steps, that permits you to use all of the functionality in the Daikon distribution.

Use the simple installation instructions if you only wish to detect invariants in Java programs. Use the complete installation instructions (which are easy to follow) if you wish to detect invariants in C or Perl programs, if you wish to run certain other programs distributed with Daikon in its ‘scripts/’ directory, or if you wish to edit and recompile the source code of Daikon itself.

Differences from previous versions of Daikon appear in the file ‘doc/CHANGES’ in the distribution. To be notified of new releases, or to join discussions about Daikon, subscribe to one of the mailing lists (see section Mailing lists).


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

2.1 Simple installation instructions

Daikon is written in Java. In order to run Daikon, all you really need is the ‘daikon.jar’ file, which is included in the distribution or can be downloaded separately from http://plse.cs.washington.edu/daikon/download/daikon.jar. Place ‘daikon.jar’ on your classpath so that Java can find it. You are now ready to use Daikon!

There are two additional requirements. You must have a Java 5.0 (or later) JVM (Java Virtual Machine). The ‘tools.jar’ file that comes with your JVM must also be on your classpath.

See section Installing Daikon, for situations where you should follow the complete installation instructions of Complete installation instructions. (Also, if you do not know how to add a jar file to your classpath, then use the complete installation instructions, which walks you through the process.)


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

2.2 Complete installation instructions

This section gives step-by-step instructions for installing Daikon.

Here is an overview of the steps. Details appear below; select the instructions for your operating system.

  1. Download Daikon.
  2. Place three commands in your shell initialization file.
  3. Optionally, customize your installation.
  4. Optionally, compile Daikon and build other tools by running make.

For more complete information on compiling Daikon, see (./developer)Compiling Daikon section ‘Compiling Daikon’ in Daikon Developer Manual.


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

2.2.1 Requirements for running Daikon

In order to run Daikon, you must have a Java 5.0 (or later) JVM (Java Virtual Machine). You must also have a Java 5.0 (or later) compiler.


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

2.2.1.1 Optional requirements for running Daikon

All the remaining requirements listed here are optional (they enable you to perform certain additional tasks with Daikon).

If you plan to use one of Daikon’s source-based front ends, then you need a compiler for whatever language your target programs are written in. For instance, if you wish to analyze C or C++ programs, you need a C or C++ compiler such as GCC. Source code and a compiler are not necessary if you plan to use one of Daikon’s front ends that work on binaries, such as Chicory (see section Java front end Chicory) or Kvasir (see section C/C++ front end Kvasir).

If you wish to edit the Daikon source code and re-compile Daikon, see (./developer)Compiling Daikon section ‘Compiling Daikon’ in Daikon Developer Manual.


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

2.2.2 Unix/Linux/MacOS installation

/item

  1. Choose the directory where you want to install Daikon; we’ll call this the daikonparent directory. In this directory, download and unpack Daikon.
     
    cd daikonparent
    wget http://plse.cs.washington.edu/daikon/download/daikon.tar.gz
    tar zxf daikon.tar.gz
    

    This creates a ‘daikonparent/daikon/’ subdirectory.

  2. Place three commands in your shell initialization file: set two environment variables and source a Daikon startup file.

    sh/bash: If you use the sh or bash shell or their variants, add these three commands to your ‘~/.bashrc’ or ‘~/.bash_profile’ file:

     
    # The full pathname of the directory that contains Daikon
    export DAIKONDIR=$HOME/daikon
    # The full pathname of the directory that contains the Java JDK; e.g.:
    export JAVA_HOME=/usr/lib/jvm/java
    source $DAIKONDIR/scripts/daikon.bashrc
    

    csh/tcsh: If you use the csh or tcsh shell or their variants, add these three commands to your ‘~/.cshrc’ file:

     
    # The full pathname of the directory that contains Daikon
    setenv DAIKONDIR $HOME/daikon
    # The full pathname of the directory that contains the Java JDK; e.g.:
    setenv JAVA_HOME /usr/lib/jvm/java
    source $DAIKONDIR/scripts/daikon.cshrc
    

    After editing your shell initialization file, either execute the commands you placed in it, or else log out and log back in to achieve the same effect.

  3. Optionally, customize other variables. The customizable variables are listed in the Daikon startup file: ‘daikon.bashrc’ or ‘daikon.cshrc’.

    You may customize them by setting environment variables, or by adding a Makefile.user file to directory $DAIKONDIR/java (it is automatically read at the beginning of the main Makefile, and prevents you from having to edit the main Makefile directly).

  4. Optionally, compile Daikon and build other tools by running make. Note that this step is not required if you only want to use Daikon with its Java front end (Chicory). This step is required for using Daikon with its C/C++ front end (Kvasir), and for other tools.
     
    cd $DAIKONDIR/java
    make
    

    This builds the various executables used by Daikon, such as the C/C++ front end Kvasir (see section Installing Kvasir) and the JDK for use with DynComp (see section Instrumenting the JDK with DynComp). For more information about compiling Daikon, see (./developer)Compiling Daikon section ‘Compiling Daikon’ in Daikon Developer Manual.

    Note that running this make command may take 20 minutes or more, depending on your computer.

    Optionally, download other executables, such as the Simplify theorem prover (http://www.hpl.hp.com/downloads/crl/jtk/).


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

2.2.3 Windows installation

To perform a complete install on Windows, it is necessary to install the Cygwin toolset. After you have installed Daikon, you can run it using either Cygwin or the regular Windows shell (see section Running Daikon under Windows).

The Cygwin toolset (available at http://cygwin.com/) contains everything you need to compile and run Unix programs under Windows. You can install Cygwin by running the appropriate setup program; either http://cygwin.com/setup-x86.exe or http://cygwin.com/setup-x86_64.exe, as determined by your machine type. The default installation of Cygwin is sufficient for installing Daikon.

  1. Choose the directory where you want to install Daikon; we’ll call this the daikonparent directory. In this directory, download and unpack Daikon.
     
    cd daikonparent
    wget http://plse.cs.washington.edu/daikon/download/daikon.tar.gz
    tar zxf daikon.tar.gz
    

    This creates a ‘daikonparent/daikon/’ subdirectory.

  2. Place three commands in your shell initialization file ‘~/.bashrc’: set two environment variables and source a Daikon startup file. Do not use a Windows shell; use the Cygwin bash shell instead.
     
    # The full pathname of the directory that contains Daikon
    export DAIKONDIR=$HOME/daikon
    # The full Unix pathname of the directory that contains the Java JDK
    export JAVA_HOME=/cygdrive/c/Program Files/Java/jdk1.6.0_20
    source $DAIKONDIR/scripts/daikon.bashrc
    

    Use the Cygwin/Unix path style (e.g., /cygdrive/c/daikon) rather than the windows path style (C:\daikon). Some users have reported problems when using pathnames with spaces. You can avoid the problem by using the ln command to add a symbolic link without spaces to Program Files.

     
    cd /cygdrive/c
    ln -s "Program Files" program_files
    

    and then the JAVA_HOME line becomes:

     
    export JAVA_HOME=/cygdrive/c/program_files/Java/jdk1.6.0_20
    

    After editing your shell initialization file, either execute the commands you placed in it, or else log out and log back in to achieve the same effect.

  3. Optionally, customize other variables. The customizable variables are listed in the Daikon startup file: ‘daikon.bashrc’ or ‘daikon.cshrc’.

    You may customize them by setting environment variables, or by adding a Makefile.user file to directory $DAIKONDIR/java (it is automatically read at the beginning of the main Makefile, and prevents you from having to edit the main Makefile directly).

    The one variable you must customize is to define the OSTYPE variable to be cygwin.

     
    OSTYPE = cygwin
    
  4. Optionally, compile Daikon and build other tools by running make. Note that this step is not required if you only want to use Daikon with its Java front end (Chicory). This step is required for using Daikon with its C/C++ front end (Kvasir), and for other tools.
     
    cd $DAIKONDIR
    make
    

    This builds the various executables used by Daikon, such as the C/C++ front end Kvasir (see section Installing Kvasir) and the JDK for use with DynComp (see section Instrumenting the JDK with DynComp). For more information about compiling Daikon, see (./developer)Compiling Daikon section ‘Compiling Daikon’ in Daikon Developer Manual in the Daikon Developer Manual.

    Note that running this make command may take 20 minutes or more, depending on your computer. On Windows, running make requires that Cygwin be installed.

    Optionally, download other executables, such as the Simplify theorem prover (http://www.hpl.hp.com/downloads/crl/jtk/), or the Z3 theorem prover (http://research.microsoft.com/en-us/um/redmond/projects/z3/; Z3 can replace Simplify but is only distributed for Windows).


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

2.2.4 Running Daikon under Windows

After you have installed Daikon under Windows (see section Windows installation), you can run it either using native Windows utilities, or using the Cygwin environment — it’s your choice.

Daikon is a command-line application (and so are its related programs, such as Chicory). You should invoke them from a command shell — either a Windows command shell or a Cygwin command shell — rather than by double-clicking their icons. In any event, double-clicking would not supply the proper arguments to the program.


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

2.2.4.1 Windows command line

The first option is to run Daikon using native Windows utilities. The is done in the normal fashion. The CLASSPATH must include either $DAIKONDIR/daikon.jar or $DAIKONDIR/java (if you have recompiled the Daikon source). The CLASSPATH should be specified in Windows format (Windows paths and semicolon separators).


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

2.2.4.2 Cygwin shell

The second option for Windows is to run Daikon using the Cygwin toolset (available at http://cygwin.com/), which contains everything you need to compile and run Unix programs under Windows. You can install Cygwin by simply running one of the setup programs (based on your machine type) found at http://cygwin.com/.

There is an incompatibility between Cygwin and programs compiled for Windows (such as Java). (The incompatibility does not exist if the program was compiled for Cygwin.) The incompatibility is that Windows programs use the semicolon (‘;’) as their path separator (for instance, for CLASSPATH), but Unix and Cygwin programs use the colon (‘:’) as their path separator.

The Makefiles used to build Daikon will change the Unix style CLASSPATH (e.g., .;/cygdrive/c/daikon/java) into a Windows style CLASSPATH (.;C:\daikon\java) when necessary. The CLASSPATH must be in Unix format for the build to work correctly.

However, when running any Java program (such as Daikon or Chicory), the CLASSPATH should be specified in Windows format. That is why the build instructions suggest specifying the CLASSPATH in the $DAIKONDIR/java/Makefile.user file — so that the required Unix definition is not part of the environment.