| Index Entry | | Section |
|---|
|
| - | | |
|---|
| -1 array index (counts from end of array): | | Variable names |
|
| . | | |
|---|
| .getClass() variable: | | Variable names |
| .inv files, tools for manipulating: | | Tools for manipulating invariants |
| .length variable name: | | Variable names |
| .NET front end: | | Celeriac |
| .spinfo file: | | Splitter info file format |
| .toString variable: | | Variable names |
|
| / | | |
|---|
| / variable (C global or file-static): | | Variable names |
|
| 6 | | |
|---|
| 64-bit AMD64 architecture, and Kvasir: | | Kvasir limitations |
|
| : | | |
|---|
| :::CLASS program point: | | OBJECT and CLASS program points |
| :::ENTER program point: | | Program points |
| :::EXIT program point: | | Program points |
| :::OBJECT program point: | | OBJECT and CLASS program points |
|
| @ | | |
|---|
| @ variable (C function-scoped static): | | Variable names |
| @NonNull type inference: | | AnnotateNullable |
| @Nullable type inference: | | AnnotateNullable |
|
| [ | | |
|---|
| [] variable name (array contents): | | Variable names |
|
| A | | |
|---|
| abstract types, for C/C++: | | DynComp for C/C++ |
| abstract types, for Java: | | DynComp for Java |
| AMD64 architecture, and Kvasir: | | Kvasir limitations |
| Annotate tool: | | Annotate |
| Annotate warning: Daikon knows nothing about field: | | Annotate |
| AnnotateNullable tool: | | AnnotateNullable |
| array type disambiguation: | | Pointer type disambiguation |
| attempted duplicate class definition error, when running Chicory: | | Attempted duplicate class definition error |
|
| B | | |
|---|
| Basic front end: | | Celeriac |
| BCEL error, when running Chicory: | | BCEL must be in the classpath |
| Beet front end for OpenAPI: | | Other front ends |
| bugs, reporting: | | Reporting problems |
|
| C | | |
|---|
| C# front end: | | Celeriac |
| C/C++ front end: | | Kvasir |
| call-site-dependent invariant: | | Conditional invariants |
| category, for debugging: | | Daikon debugging options |
| category, for debugging: | | Daikon debugging options |
| Celeriac (front end for .NET): | | Celeriac |
| Chicory (front end for Java): | | Chicory |
| CITADEL front end for Eiffel: | | Other front ends |
| class invariants: | | OBJECT and CLASS program points |
| CLASS program point: | | OBJECT and CLASS program points |
| ClassFormatError, when running Chicory: | | ClassFormatError LVTT entry does not match |
| cluster analysis for splitters: | | Cluster analysis for splitters |
| comma-delimited files: | | convertcsv.pl |
| comma-separated-value files: | | convertcsv.pl |
| command line options for Daikon: | | Running Daikon |
| comparability, for C/C++: | | DynComp for C/C++ |
| comparability, for Java: | | DynComp for Java |
| comparing invariants: | | Invariant Diff |
| comparison tool, logical: | | LogicalCompare |
| conditional invariant: | | Conditional invariants |
| confidence limit: | | Options to control invariant detection |
| configuration options: | | Configuration options |
| context-sensitive invariant: | | Conditional invariants |
| contradictory invariants: | | Contradictory invariants |
| contributors to Daikon: | | Credits |
| CreateSpinfo: | | Static analysis for splitters |
| CreateSpinfoC: | | Static analysis for splitters |
| CSharpContract output format: | | Invariant syntax |
| csv files: | | convertcsv.pl |
|
| D | | |
|---|
| Daikon knows nothing about field: warning from Annotate: | | Annotate |
| Daikon output format: | | Invariant syntax |
| Daikon version 5.8.18: | | History |
| daikon-announce mailing list: | | Mailing lists |
| daikon-developers mailing list: | | Mailing lists |
| daikon-discuss mailing list: | | Mailing lists |
| data trace files, too large: | | Large dtrace files |
| DBC output format: | | Invariant syntax |
| dcomp_rt.jar file for DynComp: | | Instrumenting the JDK with DynComp |
| debugging flags: | | Daikon debugging options |
| debugging flags: | | Daikon debugging options |
| decl format errors: | | decl format errors |
| derived variables, enabling/disabling: | | Options to enable/disable derived variables |
| derived variables, explanation of: | | Variable names |
| DerivedParameterFilter: | | Invariant filters |
| dfepl (front end for Perl): | | dfepl |
| diff, over invariants: | | Invariant Diff |
| disambiguation of array types: | | Pointer type disambiguation |
| disambiguation of pointer types: | | Pointer type disambiguation |
| disjunction: | | Conditional invariants |
| disjunctive invariant: | | Conditional invariants |
| dkconfig_ variables: | | Configuration options |
| dtrace file name: | | Chicory miscellaneous options |
| DTRACEAPPEND environment variable: | | Chicory miscellaneous options |
| DTRACEFILE environment variable: | | Chicory miscellaneous options |
| dummy invariant: | | Conditional invariants |
| dynamic comparability, for C/C++: | | DynComp for C/C++ |
| dynamic comparability, for Java: | | DynComp for Java |
| DynComp, for C/C++: | | DynComp for C/C++ |
| DynComp, for Java: | | DynComp for Java |
|
| E | | |
|---|
| Eiffel front end: | | Other front ends |
| EM64T architecture, and Kvasir: | | Kvasir limitations |
| ENTER program point: | | Program points |
| environment variable DTRACEAPPEND: | | Chicory miscellaneous options |
| environment variable DTRACEFILE: | | Chicory miscellaneous options |
| error messages: | | Troubleshooting |
| ESC/Java output format: | | Invariant syntax |
| Excel files: | | convertcsv.pl |
| EXIT program point: | | Program points |
| ‘Exiting’, in Daikon output: | | Interpreting output |
|
| F | | |
|---|
| F# front end: | | Celeriac |
| FIFO, as data trace file: | | Online execution |
| file input errors: | | File input errors |
| file name, for dtrace file: | | Chicory miscellaneous options |
| filters: | | Invariant filters |
| filters, enabling/disabling: | | Options to enable/disable filters |
| flags for Daikon: | | Running Daikon |
| front end: | | Front ends and instrumentation |
| front end for .NET: | | Celeriac |
| front end for Basic: | | Celeriac |
| front end for C#: | | Celeriac |
| front end for C/C++: | | Kvasir |
| front end for Eiffel: | | Other front ends |
| front end for F#: | | Celeriac |
| front end for Input/Output Automata: | | Other front ends |
| front end for IOA: | | Other front ends |
| front end for Java: | | Chicory |
| front end for Lisp: | | Other front ends |
| front end for Lisp: | | History |
| front end for LLVM: | | Other front ends |
| front end for OpenAPI: | | Other front ends |
| front end for Perl: | | dfepl |
| front end for Simulink/Stateflow (SLSF) block diagrams: | | Other front ends |
| front end for Visual Basic: | | Celeriac |
| front end for WS-BPEL: | | Other front ends |
|
| H | | |
|---|
| has only one value, in invariant output: | | Has only one value variables |
| hashcode type, for variables: | | Has only one value variables |
| hierarchical cluster analysis: | | Cluster analysis for splitters |
| hierarchy of program points: | | Program points |
| hierarchy, disabling: | | Options to control invariant detection |
| history of Daikon: | | History |
| HotSpot JVM: | | Out of memory |
| Hynger front end for Simulink/Stateflow (SLSF) block diagrams: | | Other front ends |
|
| I | | |
|---|
| IA-32e architecture, and Kvasir: | | Kvasir limitations |
| implication checking tool: | | LogicalCompare |
| implication invariant: | | Conditional invariants |
| implied invariant: | | Invariant filters |
| inconsistent invariants: | | Contradictory invariants |
| inference, of Nullable type: | | AnnotateNullable |
| Input/Output Automata front end: | | Other front ends |
| installing Daikon: | | Installing Daikon |
| installing Kvasir: | | Installing Kvasir |
| instrumentation: | | Front ends and instrumentation |
| instrumentation, of .NET programs: | | Celeriac |
| instrumentation, of Basic programs: | | Celeriac |
| instrumentation, of C# programs: | | Celeriac |
| instrumentation, of C/C++ programs: | | Kvasir |
| instrumentation, of Eiffel programs: | | Other front ends |
| instrumentation, of F# programs: | | Celeriac |
| instrumentation, of Input/Output Automata programs: | | Other front ends |
| instrumentation, of IOA programs: | | Other front ends |
| instrumentation, of Java programs: | | Chicory |
| instrumentation, of Lisp programs: | | Other front ends |
| instrumentation, of LLVM programs: | | Other front ends |
| instrumentation, of OpenAPI: | | Other front ends |
| instrumentation, of Perl programs: | | dfepl |
| instrumentation, of Simulink/Stateflow (SLSF) block diagrams: | | Other front ends |
| instrumentation, of Visual Basic programs: | | Celeriac |
| instrumentation, of WS-BPEL process definitions: | | Other front ends |
| instrumented JDK, for DynComp: | | Instrumenting the JDK with DynComp |
| Intel 64 architecture, and Kvasir: | | Kvasir limitations |
| inv files, tools for manipulating: | | Tools for manipulating invariants |
| invariant diff: | | Invariant Diff |
| invariant filters: | | Invariant filters |
| invariant list: | | Invariant list |
| invariant merge: | | MergeInvariants |
| invariant output format: | | Invariant syntax |
| invariant, conditional: | | Conditional invariants |
| invariant, disjunctive: | | Conditional invariants |
| invariant, dummy: | | Conditional invariants |
| invariant, implication: | | Conditional invariants |
| InvariantChecker tool: | | InvariantChecker |
| invariants, configuring: | | Other invariant configuration parameters |
| invariants, contradictory: | | Contradictory invariants |
| invariants, enabling/disabling: | | Options to enable/disable specific invariants |
| invariants, inconsistent: | | Contradictory invariants |
| invariants, list of all: | | Invariant list |
| invocation nonce: | | No return from procedure |
| IOA front end: | | Other front ends |
| irrelevant output from Daikon: | | Too much output |
|
| J | | |
|---|
| Java front end: | | Chicory |
| Java output format: | | Invariant syntax |
| java.lang.ClassFormatError, when running Chicory: | | ClassFormatError LVTT entry does not match |
| java.lang.LinkageError, when running Chicory: | | Attempted duplicate class definition error |
| java.lang.OutOfMemoryError: | | Out of memory |
| java.lang.UnsupportedClassVersionError: | | Unsupported class version |
| JDK, instrumented for DynComp: | | Instrumenting the JDK with DynComp |
| JML output format: | | Invariant syntax |
| Jtest DBC output format: | | Invariant syntax |
| JVM memory management: | | Out of memory |
|
| K | | |
|---|
| kmeans cluster analysis: | | Cluster analysis for splitters |
| Kvasir (binary front end for C): | | Kvasir |
| Kvasir installation: | | Installing Kvasir |
|
| L | | |
|---|
| large data trace files: | | Large dtrace files |
| large trace files, creating: | | Daikon runs slowly |
| large trace files, creating: | | Daikon runs slowly |
| license: | | License |
| LinkageError, when running Chicory: | | Attempted duplicate class definition error |
| Lisp front end: | | Other front ends |
| Lisp front end: | | History |
| LLVM front end: | | Other front ends |
| local variables: | | Variable names |
| local variables: | | Loop invariants |
| Logger: | | Daikon debugging options |
| Logger: | | Daikon debugging options |
| logging, for debugging Daikon: | | Daikon debugging options |
| logging, for debugging Daikon: | | Daikon debugging options |
| LogicalCompare tool: | | LogicalCompare |
| loop invariants: | | Loop invariants |
| LVTT entry does not match: | | ClassFormatError LVTT entry does not match |
|
| M | | |
|---|
| mailing lists: | | Mailing lists |
| major.minor version error: | | Unsupported class version |
| memory exhaustion: | | Out of memory |
| merge invariants: | | MergeInvariants |
| MergeESC tool, see Annotate tool: | | Annotate |
| method needs to be implemented warning: | | Method needs to be implemented |
| mux output: | | Options to control Daikon output |
|
| N | | |
|---|
| named pipe, as data trace file: | | Online execution |
| needs to be implemented warning: | | Method needs to be implemented |
| negative array index (counts from end of array): | | Variable names |
| no output from Daikon: | | No samples |
| no return from procedure, warning: | | No return from procedure |
| nonce, invocation: | | No return from procedure |
| NonNull type inference: | | AnnotateNullable |
| nonsensical values for variables: | | Variable names |
| nonsensical values for variables, guarding.: | | Quantity of output |
| nonsensical values, ignored when computing invariants: | | Interpreting output |
| Nullable type inference: | | AnnotateNullable |
|
| O | | |
|---|
| object invariants: | | OBJECT and CLASS program points |
| OBJECT program point: | | OBJECT and CLASS program points |
| observer methods, as synonym for pure methods: | | Variables in Chicory output |
| ObviousFilter: | | Invariant filters |
| on-the-fly execution, for C programs: | | Online execution |
| online execution, for C programs: | | Online execution |
| OnlyConstantVariablesFilter: | | Invariant filters |
| OpenAPI front end: | | Other front ends |
| orig() variable (pre-state value): | | Variable names |
| orig() variable (pre-state value): | | orig variable example |
| out of memory error: | | Out of memory |
| output format, CSharpContract: | | Invariant syntax |
| output format, Daikon: | | Invariant syntax |
| output format, DBC: | | Invariant syntax |
| output format, ESC/Java: | | Invariant syntax |
| output format, for invariants: | | Invariant syntax |
| output format, Java: | | Invariant syntax |
| output format, JML: | | Invariant syntax |
| output format, Jtest DBC: | | Invariant syntax |
| output format, Simplify: | | Invariant syntax |
| Output, quantity of: | | Quantity of output |
|
| P | | |
|---|
| ParentFilter: | | Invariant filters |
| Perl front end: | | dfepl |
| permanent generation (in HotSpot JVM): | | Out of memory |
| pipe, as data trace file: | | Online execution |
| pointer type disambiguation: | | Pointer type disambiguation |
| post() variable (post-state value): | | Variable names |
| post-state variables: | | Variable names |
| postcondition: | | Program points |
| pre-state variables: | | Variable names |
| precondition: | | Program points |
| printing invariants: | | Printing invariants |
| PrintInvariants program: | | Printing invariants |
| private methods: | | OBJECT and CLASS program points |
| private variables: | | Variables in Chicory output |
| problems, reporting: | | Reporting problems |
| program point: | | Program points |
| program point: | | OBJECT and CLASS program points |
| program point hierarchy: | | Program points |
| pure methods: | | Variables in Chicory output |
| Python implementation of Daikon: | | History |
|
| R | | |
|---|
| random selection for splitters: | | Random selection for splitters |
| redundant invariant: | | Invariant filters |
| reporting bugs: | | Reporting problems |
| reporting problems: | | Reporting problems |
| representation invariants: | | OBJECT and CLASS program points |
| return from procedure, warning: | | No return from procedure |
| run time, of Daikon: | | Daikon runs slowly |
| runcluster.pl program: | | Cluster analysis for splitters |
| runtime-check instrumenter: | | Runtime-check instrumenter |
| runtimechecker instrumenter: | | Runtime-check instrumenter |
|
| S | | |
|---|
| samples breakdown output: | | Options to control Daikon output |
| sampling of program point executions: | | Program points in Chicory output |
| Simplify output format: | | Invariant syntax |
| Simplify theorem prover, configuring: | | Simplify interface configuration options |
| Simplify, could not utilize: | | Simplify errors |
| Simplify, couldn’t start: | | Simplify errors |
| Simplify, installing: | | Installing Simplify |
| SimplifyFilter: | | Invariant filters |
| Simulink/Stateflow (SLSF) front end: | | Other front ends |
| slow operation, of Daikon: | | Daikon runs slowly |
| spinfo file: | | Splitter info file format |
| splitter info file: | | Splitter info file format |
| Splitters, configuring: | | Splitter options |
| Splitters, configuring: | | Debugging options |
| splitting: | | Conditional invariants |
| splitting condition: | | Conditional invariants |
| splitting conditions, cluster analysis: | | Cluster analysis for splitters |
| splitting conditions, random selection: | | Random selection for splitters |
| splitting conditions, static analysis: | | Static analysis for splitters |
| spreadsheet files: | | convertcsv.pl |
| static analysis for splitters: | | Static analysis for splitters |
| Static fields (global variables) in Java programs: | | Static fields (global variables) |
|
| T | | |
|---|
| tab-separated files: | | convertcsv.pl |
| Takuan front end for WS-BPEL: | | Other front ends |
| temporary (local) variables: | | Variable names |
| this_invocation_nonce: | | No return from procedure |
| too much output from Daikon: | | Too much output |
| trace file name: | | Chicory miscellaneous options |
| trace-purge-fns.pl script: | | Reducing program points |
| trace-untruncate program: | | Reducing executions |
| TraceSelect tool: | | Random selection for splitters |
| troubleshooting: | | Troubleshooting |
| type inference, Nullable: | | AnnotateNullable |
|
| U | | |
|---|
| Udon front end for LLVM: | | Other front ends |
| UnjustifiedFilter: | | Invariant filters |
| unmatched entries, not ignoring: | | Options to control invariant detection |
| UnmodifiedVariableEqualityFilter: | | Invariant filters |
| UnsupportedClassVersionError: | | Unsupported class version |
| useless output from Daikon: | | Too much output |
|
| V | | |
|---|
| variables, local: | | Variable names |
| variables, omit: | | Variables in Chicory output |
| variables, private: | | Variables in Chicory output |
| variables, temporary (local): | | Variable names |
| Visual Basic front end: | | Celeriac |
|
| W | | |
|---|
| warning messages: | | Troubleshooting |
| WriteViolationFile tool: | | How to access violations |
| WS-BPEL front end: | | Other front ends |
|
| X | | |
|---|
| xm cluster analysis: | | Cluster analysis for splitters |
|