2 Installing Daikon

Shortcut for the impatient: skip directly to the Installation instructions.

The main way to install Daikon is from a release, as explained in this section. (Alternately, see Source code (version control repository) in Daikon Developer Manual, to obtain the latest Daikon source code from its version control repository.) Here is an overview of the steps.

1. Download Daikon.
2. Place two commands in your shell initialization file.
3. Optionally, customize your installation.
4. Compile Daikon and build other tools. (This is optional but often needed.)

Details appear below; select the instructions for your operating system.

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

2.1 Requirements for running Daikon

In order to run Daikon, you must have a Java 8 (or later) JDK, including a Java Virtual Machine and a Java compiler.

If you wish to analyze C or C++ programs, or if you wish to edit the Daikon source code and re-compile Daikon, see Compiling Daikon in Daikon Developer Manual.

Daikon is supported on Unix environments, including Linux, Mac OS X, and Windows Subsystem for Linux (WSL). It is not supported on Windows or Cygwin.

2.2 Installation

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-5.8.18.tar.gz
   tar zxf daikon-5.8.18.tar.gz
   

   This creates a daikonparent/daikon-5.8.18/ subdirectory.

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

   We will assume that you are using the bash shell or one of its variants. Add commands like these to your ~/.bashrc or ~/.bash_profile file:

   # The absolute pathname of the directory that contains Daikon
   export DAIKONDIR=daikonparent/daikon-5.8.18
   source $DAIKONDIR/scripts/daikon.bashrc
   

   After editing your shell initialization file, either execute the commands you placed in it (e.g., run source ~/.bashrc), 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: $DAIKONDIR/scripts/daikon.bashrc.

   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. Compile Daikon and build other tools. (Strictly speaking, this step is optional, but it is highly recommended: some parts of this are required in order to infer invariants in Java programs, and other parts are needed in order to infer invariants in C programs.) First, make sure that you have satisfied the requirements in Requirements for compiling Daikon in Daikon Developer Manual. Then, run:

   make -C $DAIKONDIR rebuild-everything
   

   This builds the various executables used by Daikon, such as the C/C++ front end Kvasir (see Installing Kvasir) and the JDK for use with DynComp (see Instrumenting the JDK with DynComp). If you need more information about compiling Daikon, see Compiling Daikon in Daikon Developer Manual. If you have trouble compiling the C/C++ front end Kvasir, see See Installing Kvasir.

   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 (see Installing Simplify).