[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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).
2.1 Simple installation instructions | ||
2.2 Complete installation instructions |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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.
make
.
For more complete information on compiling Daikon, see (./developer)Compiling Daikon section ‘Compiling Daikon’ in Daikon Developer Manual.
2.2.1 Requirements for running Daikon | ||
2.2.2 Unix/Linux/MacOS installation | ||
2.2.3 Windows installation | ||
2.2.4 Running Daikon under Windows |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
2.2.1.1 Optional requirements for running Daikon |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
/item
cd daikonparent wget http://plse.cs.washington.edu/daikon/download/daikon.tar.gz tar zxf daikon.tar.gz |
This creates a ‘daikonparent/daikon/’ subdirectory.
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.
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).
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] | [ ? ] |
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.
cd daikonparent wget http://plse.cs.washington.edu/daikon/download/daikon.tar.gz tar zxf daikon.tar.gz |
This creates a ‘daikonparent/daikon/’ subdirectory.
# 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.7.0_45 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.7.0_45 |
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.
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 |
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] | [ ? ] |
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.
2.2.4.1 Windows command line | ||
2.2.4.2 Cygwin shell |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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.
Because java
is a Windows program, if you give it
a -CLASSPATH
argument it expects it to have Windows style pathnames.
An easy way to deal with this is to use the cygpath
utility:
java -cp `cygpath -wp unix/path/a:unix/path/b` <remaider of arguments> |