[
Top
]
[
Contents
]
[
Index
]
[
?
]
Table of Contents
1. Introduction
1.1 Mailing lists
2. Installing Daikon
2.1 Simple installation instructions
2.2 Complete installation instructions
2.2.1 Requirements for running Daikon
2.2.1.1 Optional requirements for running Daikon
2.2.2 Unix/Linux/MacOS installation
2.2.3 Windows installation
2.2.4 Running Daikon under Windows
2.2.4.1 Windows command line
2.2.4.2 Cygwin shell
3. Example usage for Java, C/C++, Perl, and Eiffel
3.1 Detecting invariants in Java programs
3.1.1 StackAr example
3.1.2 Using DynComp with Java programs
3.1.3 Understanding the invariants
3.1.4 Understanding DynComp
3.1.5 A second Java example
3.2 Detecting invariants in C/C++ programs
3.2.1 C examples
3.2.2 Using DynComp with C programs
3.2.3 Dealing with large examples
3.3 Detecting invariants in Perl programs
3.3.1 Instrumenting Perl programs
3.3.2 Perl examples
3.4 Detecting invariants in Eiffel programs
4. Running Daikon
4.1 Options to control Daikon output
4.2 Options to control invariant detection
4.3 Processing only part of the trace file
4.4 Daikon configuration options
4.5 Daikon debugging options
5. Daikon output
5.1 Invariant syntax
5.2 Program points
5.3 Variable names
5.3.1 orig variable example
5.4 Interpreting Daikon output
5.4.1 Redundant
5.4.2 Equal variables
5.4.3 Has only one value variables
5.5 Invariant list
5.6 Invariant filters
6. Enhancing Daikon output
6.1 Configuration options
6.1.1 List of configuration options
6.1.1.1 Options to enable/disable filters
6.1.1.2 Options to enable/disable specific invariants
6.1.1.3 Other invariant configuration parameters
6.1.1.4 Options to enable/disable derived variables
6.1.1.5 Simplify interface configuration options
6.1.1.6 General configuration options
6.2 Conditional invariants and implications
6.2.1 Splitter info file
6.2.1.1 Program point sections
6.2.1.2 Replacement sections
6.2.2 Indiscriminate splitting
6.2.3 Example splitter info file
6.2.3.1 Example class
6.2.3.2 Resulting .spinfo file
6.3 Enhancing conditional invariant detection
6.3.1 Static analysis for splitters
6.3.2 Cluster analysis for splitters
6.3.3 Random selection for splitters
6.4 Dynamic abstract type inference (DynComp)
6.5 Loop invariants
7. Front ends (instrumentation)
7.1 Java front end Chicory
7.1.1 Chicory options
7.1.1.1 Program points in Chicory output
7.1.1.2 Variables in Chicory output
7.1.1.3 Chicory miscellaneous options
7.1.2 Static fields (global variables)
7.2 DynComp dynamic comparability (abstract type) analysis for Java
7.2.1 Instrumenting the JDK with DynComp
7.2.2 DynComp options
7.2.3 Instrumentation of Object methods
7.2.4 Known bugs and limitations
7.3 C/C++ front end Kvasir
7.3.1 Using Kvasir
7.3.2 Kvasir options
7.3.3 DynComp dynamic comparability (abstract type) analysis for C/C++
7.3.4 Tracing only part of a program
7.3.5 Pointer type disambiguation
7.3.5.1 Pointer type coercion
7.3.5.2 Pointer type disambiguation example
7.3.5.3 Using pointer type disambiguation with partial program tracing
7.3.6 C++ support
7.3.7 Online execution
7.3.7.1 Online execution with DynComp for C/C++
7.3.8 Installing Kvasir
7.3.9 Kvasir implementation and limitations
7.4 Source-based C/C++ front end Mangel-Wurzel
7.4.1 Using Mangel-Wurzel
7.4.2 Mangel options
7.4.2.1 Standard compiler options for Mangel
7.4.2.2 Mangel configuration options
7.4.2.3 Mangel annotation options
7.4.2.4 Options files for Mangel
7.4.3 Pointer/array disambiguation in Mangel-Wurzel
7.4.4 Mangel-Wurzel usage notes
7.4.4.1 Using Mangel-Wurzel on Unix
7.4.4.2 Using Mangel-Wurzel on Windows
7.4.5 Interaction with Purify
7.4.6 Installing Mangel-Wurzel
7.5 Perl front end dfepl
7.5.1 dfepl options
7.6 Comma-separated-value front end convertcsv.pl
7.7 Other front ends
8. Tools for use with Daikon
8.1 Tools for manipulating invariants
8.1.1 Printing invariants
8.1.2 MergeInvariants
8.1.3 Invariant Diff
8.1.4 Annotate
8.1.5 AnnotateNullable
8.1.6 Runtime-check instrumenter (runtimechecker)
8.1.6.1 Accessing violations
8.1.7 InvariantChecker
8.1.8 LogicalCompare
8.2 DtraceDiff utility
9. Troubleshooting
9.1 Problems running Daikon
9.1.1 Too much output
9.1.2 Missing output invariants
9.1.3 No samples and no output
9.1.4 No return from procedure
9.1.5 Unsupported class version
9.1.6 Out of memory
9.1.7 Simplify errors
9.1.8 Contradictory invariants
9.1.9 Method needs to be implemented
9.1.10 Daikon runs slowly
9.1.10.1 Slow creation of large trace files
9.1.10.2 Slow inference of invariants
9.1.11 Bigger traces cause invariants to appear
9.2 Large data trace (.dtrace) files
9.2.1 Run Daikon online
9.2.2 Create multiple smaller data trace files
9.2.3 Record or read less information in the data trace file
9.2.4 Reducing program points (functions)
9.2.5 Reducing variables
9.2.6 Reducing executions
9.3 Parsing Java 5.0 code
9.4 Problems with Chicory
9.4.1 VerifyError constant pool index error
9.5 Reporting problems
9.6 Known bugs
9.7 Further reading
10. Details
10.1 History
10.2 License
10.3 Mailing lists reminder
10.4 Credits
10.5 Citing Daikon
Index
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated by
Daikon User
on
June, 23 2010
using
texi2html 1.78
.