| Index Entry | Section |
|
H | | |
| has only one value, in invariant output | 5.4.3 Has only one value variables |
| hashcode type, for variables | 5.4.3 Has only one value variables |
| hierarchical cluster analysis | 6.3.2 Cluster analysis for splitters |
| hierarchy of program points | 5.2 Program points |
| hierarchy, disabling | 4.2 Options to control invariant detection |
| history of Daikon | 10.1 History |
| HotSpot JVM | 9.1.6 Out of memory |
|
I | | |
| IA-32e architecture, and Kvasir | 7.3.9 Kvasir implementation and limitations |
| illegal constant pool index error, when running Chicory | 9.4.1 VerifyError constant pool index error |
| implication checking tool | 8.1.8 LogicalCompare |
| implication invariant | 6.2 Conditional invariants and implications |
| INCLUDE environment variable | 7.4.2.1 Standard compiler options for Mangel |
| inconsistent invariants | 9.1.8 Contradictory invariants |
| inference, of Nullable type | 8.1.5 AnnotateNullable |
| installing Daikon | 2. Installing Daikon |
| installing Kvasir | 7.3.8 Installing Kvasir |
| instrumentation | 7. Front ends (instrumentation) |
| instrumentation, of C/C++ programs | 7.3 C/C++ front end Kvasir |
| instrumentation, of C/C++ programs (deprecated) | 7.4 Source-based C/C++ front end Mangel-Wurzel |
| instrumentation, of Eiffel programs | 7.7 Other front ends |
| instrumentation, of IOA programs | 7.7 Other front ends |
| instrumentation, of Java programs | 7.1 Java front end Chicory |
| instrumentation, of Lisp programs | 7.7 Other front ends |
| instrumentation, of Perl programs | 7.5 Perl front end dfepl |
| instrumented JDK, for DynComp | 7.2.1 Instrumenting the JDK with DynComp |
| Intel 64 architecture, and Kvasir | 7.3.9 Kvasir implementation and limitations |
| inv files, tools for manipulating | 8.1 Tools for manipulating invariants |
| invariant diff | 8.1.3 Invariant Diff |
| invariant filters | 5.6 Invariant filters |
| invariant list | 5.5 Invariant list |
| invariant merge | 8.1.2 MergeInvariants |
| invariant output format | 5.1 Invariant syntax |
| invariant, conditional | 6.2 Conditional invariants and implications |
| invariant, dummy | 6.2 Conditional invariants and implications |
| invariant, implication | 6.2 Conditional invariants and implications |
| InvariantChecker tool | 8.1.7 InvariantChecker |
| invariants, configuring | 6.1.1.3 Other invariant configuration parameters |
| invariants, contradictory | 9.1.8 Contradictory invariants |
| invariants, enabling/disabling | 6.1.1.2 Options to enable/disable specific invariants |
| invariants, inconsistent | 9.1.8 Contradictory invariants |
| invariants, list of all | 5.5 Invariant list |
| invocation nonce | 9.1.4 No return from procedure |
| IOA front end | 7.7 Other front ends |
| irrelevant output from Daikon | 9.1.1 Too much output |
|
J | | |
| Java front end | 7.1 Java front end Chicory |
| Java output format | 5.1 Invariant syntax |
| java.lang.OutOfMemoryError | 9.1.6 Out of memory |
| java.lang.UnsupportedClassVersionError | 9.1.5 Unsupported class version |
| java.lang.VerifyError, when running Chicory | 9.4.1 VerifyError constant pool index error |
| JDK, instrumented for DynComp | 7.2.1 Instrumenting the JDK with DynComp |
| JML output format | 5.1 Invariant syntax |
| Jtest DBC output format | 5.1 Invariant syntax |
| JVM memory management | 9.1.6 Out of memory |
|
K | | |
| kmeans cluster analysis | 6.3.2 Cluster analysis for splitters |
| Kvasir (binary front end for C) | 7.3 C/C++ front end Kvasir |
| Kvasir installation | 7.3.8 Installing Kvasir |
|
L | | |
| large data trace files | 9.2 Large data trace (.dtrace) files |
| large trace files, creating | 9.1.10.1 Slow creation of large trace files |
| large trace files, creating | 9.1.10.2 Slow inference of invariants |
| license | 10.2 License |
| linked lists, in Chicory | 7.1.1.2 Variables in Chicory output |
| Lisp front end | 7.7 Other front ends |
| Lisp front end | 10.1 History |
| local variables | 5.3 Variable names |
| local variables | 6.5 Loop invariants |
| Logger | 4.5 Daikon debugging options |
| Logger | 4.5 Daikon debugging options |
| logging, for debugging Daikon | 4.5 Daikon debugging options |
| logging, for debugging Daikon | 4.5 Daikon debugging options |
| LogicalCompare tool | 8.1.8 LogicalCompare |
| loop invariants | 6.5 Loop invariants |
|
M | | |
| mailing lists | 1.1 Mailing lists |
| major.minor version error | 9.1.5 Unsupported class version |
| mangel driver | 7.4.1 Using Mangel-Wurzel |
| Mangel-Wurzel (deprecated source-based front end for C) | 7.4 Source-based C/C++ front end Mangel-Wurzel |
| MANGEL_DIR environment variable | 7.4.2.1 Standard compiler options for Mangel |
| MANGEL_DIR environment variable | 7.4.6 Installing Mangel-Wurzel |
| memory exhaustion | 9.1.6 Out of memory |
| merge invariants | 8.1.2 MergeInvariants |
| MergeESC tool, see Annotate tool | 8.1.4 Annotate |
| method needs to be implemented warning | 9.1.9 Method needs to be implemented |
| Microsoft Windows | 2.2.4 Running Daikon under Windows |
| mux output | 4.1 Options to control Daikon output |
|
N | | |
| named pipe, as data trace file | 7.3.7 Online execution |
| needs to be implemented warning | 9.1.9 Method needs to be implemented |
| negative array index (counts from end of array) | 5.3 Variable names |
| no output from Daikon | 9.1.3 No samples and no output |
| no return from procedure, warning | 9.1.4 No return from procedure |
| nonce, invocation | 9.1.4 No return from procedure |
| NonNull type inference | 8.1.5 AnnotateNullable |
| nonsensical values for variables | 5.3 Variable names |
| nonsensical values for variables, guarding. | 6.1.1.6 General configuration options |
| Nullable type inference | 8.1.5 AnnotateNullable |
|
O | | |
| object invariants | 5.2 Program points |
| OBJECT program point | 5.2 Program points |
| observer methods, as synonym for pure methods | 7.1.1.2 Variables in Chicory output |
| ObviousFilter | 5.6 Invariant filters |
| on-the-fly execution, for C programs | 7.3.7 Online execution |
| online execution, for C programs | 7.3.7 Online execution |
| OnlyConstantVariablesFilter | 5.6 Invariant filters |
| orig() variable (pre-state value) | 5.3 Variable names |
| orig() variable (pre-state value) | 5.3.1 orig variable example |
| out of memory error | 9.1.6 Out of memory |
| output format, Daikon | 5.1 Invariant syntax |
| output format, DBC | 5.1 Invariant syntax |
| output format, ESC/Java | 5.1 Invariant syntax |
| output format, for invariants | 5.1 Invariant syntax |
| output format, Java | 5.1 Invariant syntax |
| output format, JML | 5.1 Invariant syntax |
| output format, Jtest DBC | 5.1 Invariant syntax |
| output format, Simplify | 5.1 Invariant syntax |
|