This file lists significant user-visible changes to Daikon. (Many other changes, including most bug fixes, are not noted here.)
Further documentation can be found in:
- The Daikon Manual. Its source is file
daikon.texinfo; formatted, it appears asdaikon.htmlordaikon.pdf. It is available online at: http://plse.cs.washington.edu/daikon/download/doc/daikon.html . - The Daikon Developer Manual. Its source is file
developer.texinfo; formatted, it appears asdeveloper.htmlordeveloper.pdf. It is available online at: http://plse.cs.washington.edu/daikon/download/doc/developer.html . - The Javadoc API documentation for the source code. This is not
distributed with Daikon, but you can build it by executing the command
make -C $DAIKONDIR/java javadocIt is also available at http://plse.cs.washington.edu/daikon/download/api/ .
Daikon supports the following new invariants, over strings and sequences of strings; all of them are enabled by default:
- IsUrl
- FixedLengthString
- IsNumeric
- IsEmail
- IsDateYYYYMMDD
- IsDateDDMMYYYY
- IsDateMMDDYYYY
- IsTimeOfDay
- IsTimeOfDayWithSeconds
- IsTimeOfDayAMPM
- IsTimestampYYYYMMHHThhmmssmm
- SequenceFixedLengthString
- SequenceStringElementsAreUrl
- SequenceStringElementsAreNumeric
- SequenceStringElementsAreEmail
- SequenceStringElementsAreDateYYYYMMDD
- SequenceStringElementsAreDateDDMMYYYY
- SequenceStringElementsAreDateMMDDYYYY
- SequenceStringElementsAreTimeOfDay
- SequenceStringElementsAreTimeOfDayWithSeconds
- SequenceStringElementsAreTimeOfDayAMPM
- SequenceStringElementsAreTimestampYYYYMMHHThhmmssmm
Improved DtraceDiff tool.
Bug fixes and implementation details:
- BCEL update to 6.8.1.
- CheckerFramework update to 3.42.
- fixed a problem with DynComp (#532)
Support Rocky Linux.
All Daikon tools now work with Java 20.
All Daikon tools now work with Java 18.
Fixed a bug in DynComp's command-line processing.
DynComp now supports the JUnit 5 test framework.
Bug fixes and implementation details:
- Valgrind update from 3.17.0 to 3.19.0.
- Binutils update from 2.37 to 2.39.
- fix DynComp command line input (#399)
- fix Fjalar support for Ubuntu 22.04 (#56)
All Daikon tools now work with Java 17. Javadoc Doclets are supported for Java 8, 11 and 17. (Later versions of Java probably work, but are not tested.)
Daikon:
- Reduced output for --show-progress; added --show-detail-progress option.
Bug fixes and implementation details:
- Update bcel util to version 1.1.15 (Support for Groovy objects and improvements to local variable table generation).
DynComp can now handle synthesized bridge methods. Merge comparability fix for fields.
Cleaned up the documentation of invocation options for Chicory and DynComp.
Bug fixes and implementation details:
- Improved implementation of DynComp runtime clone methods (Daikon #358).
- Update JUnit and Hamcrest to be compiled for JDK 8 (Daikon #346, #364).
- Check for too large to instrument (#343).
- Fix dcomp equals (#338).
- Valgrind update from 3.16.1 to 3.17.0. (Daikon #327, Fjalar #51).
- Binutils update from 2.35.1 to 2.37 (Fjalar #53, Fjalar #54).
- Have Chicory and DynComp use same code for ppt-omit and ppt-select (#342).
- Update bcel util to version 1.1.12 (#344) (Includes several fixes to local variable table generation).
Added DynComp --dump option, which dumps instrumented classes to a file.
Improved DynComp comparability results for JDK 11.
DynComp handles lambdas (Java anonymous functions).
Improved DynComp support for JUnit test framework.
Removed DynComp option --no-primitives.
Removed support for the obsolete version 1 file format.
Moved the SplitDtrace class from the unnamed package to the daikon/ package.
Chicory and DynComp:
- Improved support for old class files (e.g., compiled by Java 5).
Fjalar/Kvasir:
- Added support for systems with a secondary target of X86.
- Added support for binaries generated by the clang compiler.
- Improved documentation on gcc compiler options.
- Updated the underlying Binutils infrastructure to version 2.34.
Improved installation instructions.
Updated Valgrind from 3.14.0 to 3.15.0.
Daikon runs under both Java 8 and Java 11.
Running Daikon is no longer supported on Windows or Cygwin. Use Windows Subsystem for Linux (WSL) instead. You can still run a front end on Windows to generate a trace file, but you should run Daikon on a Unix-like system to process that trace file. We welcome community support for the Windows and Cygwin operating systems.
Daikon no longer requires the JAVA_HOME environment variable to be set,
if the javac executable is on the path.
Updated the readelf, Valgrind, and BCEL libraries. This should improve compatibility with operating systems and C versions.
The Daikon instructions no longer suggest to set CLASSPATH, which is bad
style. Instead, a new environment variable DAIKON_CLASSPATH is set by
daikon.bashrc, if you choose to use that script.
The DAIKONDIR environment variable is not needed. It is only used for
documentation purposes in the manual.
Daikon runs on Cygwin. However, the Daikon developers no longer support building Daikon on Cygwin, which requires tricky translation between Windows and Unix paths. If you want to develop Daikon on a computer that runs Windows, we suggest using Linux in a virtual machine, or Linux Subsystem for Windows (available since August 2016).
Daikon now requires Java JDK 8; Java JDK 7 is no longer supported.
Implementation detail: Daikon no longer uses the monolithic plume-lib repository, which has been split into smaller ones such as plume-scripts.
DynComp:
- Fix issue #129 - Too many parameters for an annotation method.
Fjalar/Kvasir:
- Fix issue #27 - Incorrect categorization of some SIMD instructions.
Eliminate reliance on plume.jar file, in favor of smaller libraries
(checklink, html-tools, options, plume-util, etc.).
Fjalar/Kvasir:
- We updated the underlying Binutils infrastructure to version 2.30.
The --wrap_xml command-line option now produces valid XML.
It is no longer necessary to set the DAIKONDIR environment variable when
using or building Daikon.
Fjalar/Kvasir:
- We updated the underlying Valgrind infrastructure to version 3.13.0.
- We updated the underlying Binutils infrastructure to version 2.29.1.
- Improved Ubuntu 17.10 support.
Support was added for Ubuntu 17.10. Please see User Guide notes about using
the -no-pie option on gcc.
DynComp:
- Fixed a few DynComp bugs.
Chicory:
- Fixed a couple of Chicory bugs.
Updated our internal version of BCEL to match Apache version 6.1. Daikon will fail if some other version of BCEL is found first on the classpath.
Chicory:
- Improve support for programs with multiple threads.
Fjalar/Kvasir:
- We updated the underlying Binutils infrastructure to version 2.28.1.
- Fix issue #10
Chicory and DynComp:
- Refactored some instrumentation code. Includes a few bug fixes.
DynComp:
- Fixed a few DynComp bugs.
DynComp:
- Fixed a few DynComp bugs.
Kvasir:
- We updated the underlying Binutils infrastructure to version 2.27.0.
DynComp and Chicory:
- Improve support for programs with multiple threads.
- Improve support for older (Java5) class files.
Kvasir:
- We updated the underlying Valgrind infrastructure to version 3.12.0.
DynComp:
- Fixed several issues related to StackMaps.
- Made several performance improvements.
Chicory:
- Allow for a ConcurrentModificationException when attempting to get the contents of a subList.
Updated our internal version of BCEL as part of StackMap fix.
Kvasir:
- The option
--with-dyncomphas been changed to--dyncompand is now the default. Use--no-dyncompto not run the DynComp portion of Kvasir. - Clarified instructions for building the sample Fjalar tool.
DynComp:
- The
--compare-sets-fileoption has been renamed to--comparability-file. - The
--trace-sets-fileoption has been renamed to--trace-file. - The
--no-cset-fileoption has been removed, this is now the default. - The
--no-jdkoption has been removed, use--rt-file=NONEinstead.
Documentation:
- Improved discussion of DynComp and comparability sets.
The changes in this release reflect an increased emphasis on using the DynComp tool for both Java and C/C++.
Daikon:
- Several improvements to the DynComp for Java tool, including:
- support for multi-threaded programs
- improved support for user programs that throw exceptions
- recover gracefully from methods too large to instrument
Documentation:
- Simplified and improved the Installation chapter of the User Guide.
- Modified the Example usage chapter of the User Guide to more accurately describe the tool options and expected outputs.
- Fixed calculation of a class's fields to include fields of its superclass(es).
- Corrected files included in daikon.tar to support building the documents.
- Corrected behavior of the calc_possible_invs configuration option.
Fixed numerous DynComp bugs.
daikon.jar now includes Apache Commons BCEL 6.0; previously it used a locally-modified version of BCEL. We have removed the "--default-bcel" command-line option; Daikon will fail if some other version of BCEL is found on the classpath.
A new front end for LLVM is available. See https://github.com/markus-kusano/udon. You can use it with any program that can be compiled to LLVM.
Chicory command-line argument --instrument-clinit causes Chicory to output empty dtrace records when static initializers are entered and exited. This is useful for clients that use Chicory to trace method entry and exit.
Daikon does stricter checking of its input files. Older versions of Kvasir and Chicory create invalid .decls or .dtrace files, which Daikon now rejects. If this happens, re-run the front end to create new, correct files.
Updated the Binutils-based code in Fjalar/Kvasir to v2.26.1. There should be no user-visible differences in the behavior of Kvasir.
Several options to the Kvasir DynComp feature (--with-dyncomp) were renamed to be more consistent:
--gc-num-tags=>--dyncomp-gc-num-tags--no-dyncomp-gc=>--dyncomp-gc-num-tags=0--dyncomp-fast-mode=>--dyncomp-approximate-literals--separate-entry-exit-comp=>--dyncomp-separate-entry-exit--dyncomp-dataflow-only=>--dyncomp-interactions=none--dyncomp-dataflow-comp=>--dyncomp-interactions=comparisons--dyncomp-units=>--dyncomp-interactions=units- [new option; is the default] =>
--dyncomp-interactions=all
Improved portability:
- support g++ 6.1
- support Fedora 23
- support newer version of jdk8
Miscellaneous bug fixes and minor improvements.
A new front end for Simulink/Stateflow (SLSF) block diagrams is available. See https://github.com/verivital/hynger .
Fjalar/Kvasir:
- DynComp has been modified to improve its accuracy and correct its garbage collection routine.
Miscellaneous bug fixes and minor improvements.
Daikon:
- Command-line argument
--user-defined-invariantmakes Daikon compute a user-defined invariant in addition to those that are built in to Daikon. - Command-line argument
--disable-all-invariantsdisables all of Daikon's built-in invariants. Subsequent command-line options may enable some of them.
Fjalar/Kvasir:
- Minor changes to support Scientific Linux.
Documentation:
- Improved the discussion in the Troubleshooting chapter of the User Guide on how to respond to "Could not find or load main class."
Daikon:
- We have improved splitter processing. Splitter expressions containing 'orig' now work correctly. Also, A splitter expression containing references to a parameter and an unqualified member variable with the name will now work correctly.
Kvasir:
- We updated the underlying Valgrind infrastructure to version 3.11.0. Users of Kvasir to analyze C/C++ codes should not see any differences in behavior from the previous version.
Documentation:
- Improved discussion of program points.
We have decided to deprecate support for 32-bit hosts.
- Fjalar/Kvasir, the C/C++ front end for Daikon, no longer builds on a 32-bit platform and we will no longer support the 32-bit version of this tool.
- At the present time, Chicory and Daikon continue to build and run on a 32-bit platform, but we have stopped testing this configuration and make no guarantees for the future.
This is an update to 5.2.24 to correct a small problem in Chicory. It was inadvertently adding extra information to its output files. This did not cause Daikon to operate incorrectly. It only made the data files larger than necessary.
Documentation:
- Added more examples of invariants.
- Improved instructions on building Daikon and Kvasir.
We have updated the Daikon tool set to include a newer version of BCEL. If Chicory throws an error such as the following: "BCEL must be in the classpath. Normally it is found in daikon.jar." Then the problem is most likely that your classpath contains a previous version of daikon.jar or plume.jar.
Documentation:
- Improved instructions on building Daikon and Kvasir.
Daikon:
- Avoid ConcurrentModificationException in the FileIOProgress thread.
- Makefile in distribution is now the same as in a cloned repository.
Kvasir:
- Eliminated OS-specific regression test failures.
Documentation:
- New manual section "Detecting invariants when running a Java program from a jar file"
- Restructured developer manual section "Requirements for compiling Daikon"
Distribution:
- The distribution contains new directories doc/www, java/jtb, and java/lib, which makes the directory layout more like the repository's.
Chicory:
- Improved handling of Java code containing synchronized locks.
- Improved handling of Java initialization methods containing calls to other initialization methods.
Daikon:
- The
--shiny-printoption was renamed--abridged-varsto match the documentation.
Kvasir:
- We made some changes to the DynComp tool to improve the accuracy of the comparability information. Occasionally, the system loader was causing unrelated items to be placed in the same comparability set.
Daikon: We have improved splitter verification testing.
Documentation: Improved discussion of splitters
Daikon: We have improved splitter file processing.
Documentation: Improved discussion of splitters
Chicory:
- Modified generation of comparability values when using input from DynComp
.decls file via
--comparability-fileoption. When the resulting .dtrace file is fed to Daikon, the number of uninteresting invariants is reduced.
DynComp:
- Correctly identify methods that are in the Java SE Development Kit (JDK).
- Fix problems with non-local field access.
- Fix problems with use of some javax classes.
LogicalCompare:
- The "debug-all" option has been changed to "debug" to be consistent with the other Daikon tools.
Changes relevant to building from source:
- Now support gcc 5.1.1 and Fedora 22.
The Daikon and Fjalar version control repositories have moved from Google Code to GitHub, and from the Mercurial version control system to Git. You should not use any old clone of the Mercurial repositories. You can obtain the new version control repositories by running:
git clone https://github.com/codespecs/daikon.git
git clone https://github.com/codespecs/fjalar.git
The location of the Celeriac front end has changed: https://github.com/codespecs/daikon-dot-net-front-end
The Daikon .tar and .zip release file names now include the version number; e.g., daikon-5.2.8.zip instead of daikon.zip. The same renaming is true of the top-level directory within these archive files.
Documentation:
- The developer manual has an improved discussion of comparability values.
- Developer manual section A.5, "Example files", has been updated.
- The user manual has an improved discussion of mixed .decls and .dtrace files. This includes some clarification of how to use the output(s) of Chicory and DynComp with Daikon.
- Improved formatting of Javadoc.
Daikon:
Changed default value of --suppressSplitterErrors command-line option to true.
Chicory: Improved support for nested classes. When processing an object of inner class type, Chicory outputs outer class fields just like inner class fields.
DynComp: Fixed a problem with DynComp not working properly with JDK 8.
Changes relevant to building from source: The plume-lib library's version control repository has moved. If you are currently building Daikon from a clone of our repository, run:
cd $DAIKONDIR
hg pull -u
rm -rf $DAIKONDIR/plume-lib
make -C $DAIKONDIR compile
Tools that process invariant files: Fixed a problem with Annotate and improved its output
The parser used by several tools (Annotate and RuntimeChecker, for example) has been improved to understand the 'diamond operator' ("<>") used for type inference in generic instance creation.
Documentation: Improved discussion of splitters
The location of the Celeriac front end has changed: https://github.com/melonhead901/daikon-dot-net-front-end
Tools that process invariant files:
Renamed LogicalCompare program's --cfg command-line argument to
--config_option, for consistency with other programs in the Daikon suite.
Improved the documentation for the Daikon runtimechecker tool.
Kvasir C/C++ front end:
Fixed a problem with creating pointer type disambiguation files when
using the --disambig and --disambig-file options to Kvasir.
Updated the Binutils-based code in Fjalar/Kvasir from v2.24 to v2.25. There should be no user-visible differences in the behavior of Kvasir.
Removed documentation for the galar front-end tool as it is no longer supported.
Bug fixes:
Fixed an intermittently occurring problem in Chicory with instrumenting Java methods containing a switch.
Fixed several Daikon issues:
- #18: runtimechecker should not instrument abstract classes
- #19: runtimechecker parser problem with ">" characters
- #20: runtimechecker problem with 'Is power of 2'
- #22: runtimechecker fails on inner classes with multiple constructors
- #23: runtimechecker crashes when foreach variable has a final modifier
We updated the underlying Valgrind infrastructure to version 3.10.1 (build 14784). Users of Kvasir to analyze C/C++ codes should not see any differences in behavior from the previous version.
We made various improvements to the documentation.
Splitters now properly support unqualified member variables within .spinfo files.
Fjalar support improved for C++ static const items. (For more information, see Daikon issue #37: #37.)
Updated bcel.jar (within plume.jar) for some minor improvements in JDK 8 support.
Fjalar now builds correctly on Ubuntu 14.10. Improved installation instructions. Improved documentation on Simplify tool. Chicory and DynComp now support Java/JDK 8. (tested with 1.8.0-b129)
Celeriac, Daikon's front end for .NET programs, works under Mono. See https://github.com/codespecs/daikon-dot-net-front-end .
The declaration file format supports five new variable-info fields:
- min-value
- max-value
- min-length
- max-length
- valid-values
These specify what possible values may appear in the trace file, and they enable Daikon to suppress invariants that are obvious due to, for example, programming language limitations on the values for a particular type. Thanks to Antonio Garcia Dominguez for contributing this feature.
The Daikon installation tests now pass when the current locale is not en_US.
We have fixed bugs in Daikon splitter file processing. For example, a splitter condition can now reference a local variable and a global variable with the same name. (The global variable, of course, requires a class name prefix.)
If you work from a clone of the repository, as opposed to downloading the
Daikon release, then there needs to be a symbolic link named 'fjalar'
from the Daikon clone to the Fjalar clone. After this change, you need to
regenerate the fjalar Makefiles.
To accomplish all of this, run the following commands:
cd $DAIKONDIR
rm -f kvasir # remove old link
ln -s ../fjalar fjalar
cd $DAIKONDIR/fjalar/valgrind
./autogen.sh
./configure --prefix=pwd/inst
We have fixed some problems in Kvasir with C++ code. We now correctly support unnamed parameters and subclasses that add no additional data members.
We have modified the output of txt-cset and txt-trace so that the invariants detected match those of the decls-DynComp output.
We have improved Daikon splitter file processing. In particular, the handling of arrays has been improved.
Daikon will now build on Macs with a non-gcc C++ preprocessor.
We have added a section to the documentation on how to write your own tool to manipulate a .dtrace file.
The manual contains a link to Takuan, a Daikon front end for WS-BPEL tool process definitions.
A large number of small corrections were made to the Javadoc annotations in the Daikon source tree. This will most often manifest in the HTML documentation as supplying information that was previously missing.
We have fixed a problem in Kvasir with C++ static members. This should provide more accurate invariants in these cases.
We have fixed a problem in DynComp with lambda expressions in Java 8 programs. Previously, this syntax would cause a program fault.
A section has been added to the Daikon User Manual describing how to deal with a "duplicate class definition error" when running Chicory.
We have fixed a problem (Daikon issue #33) that would cause Chicory to crash on input of the form:
private static final Boolean name = false;Improved StackMap support.
- for methods
- for BASTORE instruction Improved Kvasir (C/C++ Daikon front end) support for 32bit hosts.
Improved StackMap support.
- Both Daikon and DynComp can now process a wider variety of Java 7 generated StackMaps. Documentation updates and cleanup.
- Added material on CSharpContracts; usage and copyright.
Daikon can now infer code contracts for .NET programs, such as C# programs. You will require the Celeriac front end: https://github.com/codespecs/daikon-dot-net-front-end In the past, when using Celeriac, you were required to use a special version of Daikon; now you should just use the regular version of Daikon.
DynComp for Java now works with Java 7. Chicory already worked with Java 7, but the DynComp component did not work with Java 7 until this release. (This is the fix for Daikon issue #24.)
General: We have modified the directory layout relationship between Daikon and Fjalar/Kvasir. If you acquire Daikon and Fjalar via their Mercurial repositories, you need to perform the following steps to adjust a symbolic link. (If you download daikon.zip or daikon.tar.gz from the Daikon distribution site, you are not affected.) For repository users, perform the following steps:
cd $DAIKONDIR
make -C kvasir uninstall distclean
rm kvasir
<hg fetch of the latest daikon and fjalar files>
cd $DAIKONDIR
ln -nsf ../fjalar kvasir // replace "fjalar" with your repository name, if different
make kvasir
Daikon: This release contains fixes for Daikon issues #10, 29 and 30. See: #10 #29 #30
Daikon: This release contains a fix for Daikon issue #28. See: #28
Fjalar: We updated our object code reader to match version 2.24 of the GNU binutils. Updated the source copyrights. Added two more regressions tests. Fixed Daikon issue #28.
Users of Kvasir to analyze C/C++ codes should not see any differences in behavior from the previous version.
Documentation: Lots of changes to correct spelling and .texinfo tag usage. No significant content changes were made.
Daikon: This release contains a fix for Daikon issue #27. See: #27
Fjalar: We updated the underlying Valgrind infrastructure to version 3.9.0 (build 13710). In addition, we cleaned up our sources so that there are no compiler warnings when building Valgrind/Fjalar/Kvasir. As Fjalar is based on the Valgrind tool "memcheck", we have seen one new memory usage error when running our tests. Other than this slim possibility, users of Kvasir to analyze C/C++ codes should not see any differences in behavior from the previous version.
Documentation: We no longer distribute PostScript formatted versions of the documentation.
General
- Improved documentation and installation script for Cygwin.
- Added corrected version of inv-cvs to new drop site.
- Several documentation improvements.
Documentation
- Fixed broken links between the two daikon documents.
- Updated some URLS to change MIT => UW.
- Clarified that you must use Java version 7.
- Removed documentation on Csh in favor of Bash.
- Improved pdf output - now includes bookmarks and hyper-links.
- Added split html document versions to drop.
- Improved General Index(s).
Highlights
- Celeriac is a new front end for .NET languages (C#, F#, and Visual Basic).
- The Kvasir front end for C works with current Linux distributions.
- Daikon releases can be found at http://plse.cs.washington.edu/daikon/.
- The bug tracker has moved to Google Code, and mailing lists to Google Groups.
General
The Daikon distribution is now hosted at the University of Washington: http://plse.cs.washington.edu/daikon/
Bug reporting is done using GitHub issue trackers: https://github.com/codespecs/daikon/issues/ https://github.com/codespecs/fjalar/issues/ Problems with Kvasir should be submitted against the Fjalar product. All other problems should be submitted against the Daikon product.
Mailing lists have migrated to Google Groups: daikon-announce@googlegroups.com daikon-discuss@googlegroups.com daikon-developers@googlegroups.com To subscribe, go to the appropriate site below and "Apply to join group": https://groups.google.com/forum/#!forum/daikon-announce https://groups.google.com/forum/#!forum/daikon-discuss https://groups.google.com/forum/#!forum/daikon-developers (daikon-developers is for people doing Daikon development.)
Renamed the bin/ directory to scripts/.
Chicory front end for Java
Updated for Java 7.
WARNING: Although Chicory proper works with Java 7, DynComp does not yet work with Java 7. As a workaround, you can compile your code with: javac -target 5 -source 5 ... If this is a problem for your project, please add a comment to the issue tracker to let us know: #24
Kvasir front end for C/C++
User visible changes
Support for more recent versions of Linux (tested with Fedora 19).
Support for more recent versions of GNU tools (tested with gcc 4.8.2
and glibc 2.17).
Mangel-Wurzel front end for C/C++
It has not been supported for almost a decade, so we have removed all references to the Mangel-Wurzel front end from the documentation.
Documentation
We have enhanced the documentation on using Daikon with Eclipse.
We no longer distribute Texinfo-formatted "info" versions of the documentation. However, the targets remain in the Makefile if you wish to make your own.
We have added a section to the developer documentation on how to make a distribution.
- Fix for stack map problem in Chicory.
- The bin directory is now called scripts to be consistent with the Google
- Code repository and the documentation.
- Fix for stack map problem in Chicory.
- Support for more recent versions of Linux (tested with Fedora 17).
- Support for more recent versions of gnu tools (tested with gcc 4.7.2 and glibc 2.17).
- Support for Java 7.
- Updated readelf support to version 2.23.2.
- Updated underlying Valgrind from revision 11017 to 12996 and VEX from revision 1953 to 2538. Together, this represents Valgrind 3.8.1.
- Many improvements and bug fixes to Chicory, the Java front end for Daikon.
User-visible changes
Added new invariants: CompleteOneOfScalar, CompleteOneOfString
Added configuration variable daikon.FileIO.rm_stack_dups.
When calculating the confidence value for an invariant, Daikon sometimes estimates the number of possible unique values that have been seen. This calculation has been changed to better handle variable that are often missing. In particular, invariants over combinations of variables that are never present in the same sample, will have a zero confidence and will thus not normally be printed.
Improved documentation about: handling large data trace files or slow Daikon runs; the confidence of each invariant; and the types of program point declarations and their relationship to the program point hierarchy.
Daikon uses the JAVA_HOME environment variable, rather than JDKDIR.
Non-user-visible changes
Extracted utilMDE and other utilities into a new library named plume-lib, which makes it easier to use in other programs. See https://mernst.github.io/plume-lib/.
Daikon now type-checks with the Nullness Checker (which is part of the Checker Framework), with just a few suppressed warnings. As far as we know Daikon is the largest program ever to be verified in this way.
Interned some string variables when de-serializing an invariant file, saving an appreciable amount of memory.
Documented Chicory options --boot-classes=REGEX, --linked-lists.
User-visible changes
Fixed an issue where Fjalar would not correctly traverse variables when using the var-list-file option.
The var-list-file can specify different global variables for different functions, rather than having to specify the same set of global variables for all of a program.
Kvasir's support for GCC 4.4 has been further improved.
User Documentation
Added documentation for several previously undocumented Kvasir command line options.
Fixed a bug when searching for dcomp_premain.jar. The jar file will now be found if it is anywhere in the classpath.
Added --verbose option that will print all samples that violate an
invariant.
Kvasir's support for GCC 4.4 has been improved.
User-visible changes
The output of variables declared as constant can now be suppressed via the "--ignore-constants" flag.
Bug fixes
Fixed an issue where Fjalar would not print variables declared constant for binaries created with some versions of g++.
Fixed comparability errors which occurred when Kvasir was run with dyncomp on an x86-64 host.
Kvasir's support for x86-64 hosts and C++ programs has been improved.
User visible changes
Kvasir now has limited support for non-local exits such as setjmp/longjmp and C++ Exceptions. Kvasir will correctly detect if a function has been exited by non-local means and not print an exit program point for the function but continue printing other functions as normal. Previously Kvasir would stop printing program points after the first non-locally exited function.
Added support for multi-threaded C/C++ programs.
Kvasir's now fully supports x86-64 hosts and running x86-64 binaries.
Improved Kvasir's speed when working with large C++ binaries.
Bug fixes
Fixed an issue where Kvasir would print incorrect values for floating point numbers.
Fixed an issue where Kvasir would print incorrect values for parameters to C++ constructors.
Fixed a memory leak in Fjalar's processing of variable names.
Fixed a crash that would sometimes occur when processing C++ programs with large amounts of debugging information.
User Documentation
Added an explanation of how additional data changes invariant output.
Support for GCC 4.3+ created binaries has been improved for Kvasir.
Documentation
Appendix A (File Formats) of the Daikon user manual was moved to
the developers manual.
User visible changes
Kvasir should now print more sensible traces for binaries created
with GCC 4.3.x and 4.4.x.
Bug fixes
Fixed an issue where Kvasir would not detect entry to a function if
it's body consisted of only a loop.
Kvasir now supports binaries created with GCC 4.0+ and glibc versions 2.2 to 2.10. The Daikon user manual was updated for clarity and completeness. Bugs were fixed in Daikon, Kvasir, and Chicory.
Documentation
The installation section of the user manual was rewritten .
A more complete explanation of nonsensical values was added to
Appendix A (File formats).
Bug Fixes
The declaration version (decl-version) specification only needs to
be specified once if multiple input files are used. If it is specified
in each file, each specification must be the same.
The Quant code (used when adding invariant checks to the original
source) did not support character comparisons. This problem has been
resolved.
Bug Fixes
In some circumstances Chicory would not handle the children of static
variables that were referenced through multiple variables (such
as a parameter and an instance variable). This problem has been
resolved.
Sampling now works correctly with applications with multiple threads
User visible changes
Starting with this release, Kvasir is more closely tracking
the upstream development of Valgrind, with the aim of getting
Valgrind portability fixes into our releases in a more timely
manner. In particular, this release includes the fixes from
Valgrind's 3.4.1 stable release including initial support for
glibc version 2.10.
Kvasir is now able to correctly output dtrace files for binaries
produced with GCC 4.0+.
Variables declared with the "register" attribute should now be
handled correctly.
Bug fixes
Fixed an issue where the decls header wasn't printed if Kvasir was
run with DynComp.
Fixed an issue where extra decls headers were printed when Kvasir
was in append mode.
Fixed an issue where Kvasir attempted to print variables for which
there was no debugging information available.
Support for Daikon and DynComp for Java has been improved for Mac OS X. The Daikon user and developer manuals were enhanced.
Documentation
A section was added describing approaches for writing automated
tools that process Daikon output
A new section (5.4.3) was added explaining the "Has only one value"
invariant.
Detail was added to the section (6.5) on Loop invariants
Information on compiling Daikon for Mac OS X was added to
section 2.1 of the Daikon Developers manual.
Documentation
Information describing how to create an instrumented JDK on Mac OS X
was added to Section 7.2.1 (Instrumenting the JDK with DynComp)
Bugs were fixed in Chicory and AnnotateNullable. Daikon's documentation was improved.
Bug fixes
A problem the occurred when a purity file is specified
was resolved.
In some circumstances, when classes are dynamically created at
run time, Chicory would incorrectly determine that the class
was a user class (i.e., not part of the JDK). This would
result in classloader areas. This has been resolved
Documentation
The Daikon user manual was improved with more detailed information
on compiling Daikon, creating implications, and the information
required with bug reports.
Bug fixes
A null pointer exception that occurred in the case of the
default package was fixed.
Resolved a number of problems in the build scripts and documentation for a complete Windows installation.
Bug fixes
Some build problems on Windows were fixed. Checks were added to
ensure that the correct version of find is found and the OSTYPE
is set correctly.
Documentation
The complete installation for Windows now requires Cygwin. The
instructions were largely rewritten to make the required setup
clear (particularly the format of filenames and paths).
Some new String invariants were added to Daikon.
User visible changes
Added elementwise String comparison (equal, lessthan, greaterthan,
lessthanequal, greaterthan equal) invariants (enabled by default).
Added a SubString invariant and an elementwise SubString invariant
(disabled by default)
A new front end for Eiffel is available and a new tool (MergeInvariants) for merging serialized invariant files was added. Some modifications and bug fixes were made to the AnnotateNullable tool and some Daikon bugs were fixed.
User visible changes
A new front end for Eiffel programs is available. See
https://se.inf.ethz.ch/people/polikarpova/citadel/ .
A new tool (MergeInvariants) for merging serialized invariant files has
been added. See section 8.1.2 of the user manual for more information.
The command line options for the AnnotateNullable tool have been
slightly changed and some bugs have been fixed. See section 8.1.5 of
the user manual for more information.
Daikon permits duplicate program point definitions in trace files as
long as they have exactly the same variables as the previous definition.
Bug fixes
Some minor errors in the code that merges results from the program point
hierarchy were resolved.
A problem with suppressors that are not valid over their input
types was fixed. Suppressors that are not valid over their input types
are no longer considered. Using such suppressors could cause otherwise
valid invariants to be missed.
Kvasir was updated to create the new format for declaration records. Kvasir was also upgraded to support newer versions of glibc.
Kvasir has been updated to produce trace files using the new format for declaration records. This format should allow for future improvements with regards to readability. the old format can be produced using the flag "--old-decls-format"
User visible changes
The new declarations format has allowed for some improved handling
for determining object invariants in C/C++. Kvasir can now produce
object declarations for C/C++ structs. This option is, by default,
off and can be turned on with "--parent-records"
Kvasir's version of Valgrind has been updated to support newer versions
of glibc. Kvasir should now support all versions of glibc supported by
Valgrind 3.3.1(glibc 2.2-28)
Bug fixes
Fixed an issue with VarComparability being inserted into a dtrace file
twice when in append mode
Fixed an issue where C++ references were not being dereferenced
correctly leading to memory locations to appear in trace files
as opposed to the value being referenced
Daikon's set of invariants and derived variables enabled by default was changed to provide more relevant invariants. Configuration options were added for some invariants. Bugs were fixed in Daikon and Chicory.
User visible changes
The following less common invariants are no longer enabled by
default: SubSequence, SuperSequence, FunctionBinary, NoDuplicates,
SeqIndex, Divides, Square, ZeroTrack, BitwiseAndZero,
BitwiseComplement, BitwiseSubset, and ShiftZero. Their
configuration options can be used to enable them if desired.
Individual enable configuration options were added for the Numeric
invariants Divides, Square, ZeroTrack, BitwiseAndZero, BitwiseComplement,
BitwiseSubset, and ShiftZero. Also for the Range invariants Even and
PowerOfTwo.
The other Range invariants (which provide information similar to the
Upper/LowerBound and OneOf invariants and are used for non-instantiating
suppressions) are enabled if their corresponding Bound
or OneOf invariants are enabled. The invariants EqualZero, EqualOne,
EqualMinusOne, are enabled if OneOf is enabled. The invariants
GreaterEqualZero, GreaterEqual64, BooleanVal, and Bound0_63 are enabled
if the Upper/LowerBound invariants are enabled.
The Range invariants PowerOfTwo and Even will now print if they
are enabled. A dynamic obvious check was added so that they are
considered obvious if there is a OneOf invariant over the same variable.
Modified the CommonSequence invariant to not consider common sequences
over hashcodes (pointers). This can be overridden with the
daikon.inv.unary.sequence.CommonSequence.hashcode_seqs configuration
option.
Bug Fixes
- Fixed the Simplify output for StringLength derived variables
- Fixed a bug where Boolean constants were not parsed correctly in
the new declaration format
- Any suppressions that included "result == arg1" and "arg1 == arg2"
were augmented to include "result == arg2". Invariants are not
necessarily transitive due to missing variables. Under certain
conditions this problem could lead to an assertion failure in Daikon.
- Fixed some problems with supporting user implementations of
java.util.List as sequences.
Bug Fixes
- Prevented unintended recursion that occurred if processing a variable
in one dtrace record called instrumented code (e.g., calling toArray
as part of processing a list or pure functions). Recursive calls to
enter() or exit() are simply ignored.
A number of bugs were fixed in Daikon, Chicory, and DynComp. The user manual was improved. Support for IOA format was removed from Daikon.
User visible changes
- Removed support for IOA format
Bug fixes
- Removed unintentional dependency on 1.6 JDK routines. Only Java
1.5 is required to compile or run Daikon.
Documentation
- Added troubleshooting section when expected invariants are not
reported.
Bug fixes
- Fixed typo in comparability type when comparability information
is included.
Bug fixes
- Fixed the classpath specification on windows to use the correct
path specifier.
- Changed handling of the sub-process so that stdout and stderr output
is not mixed character by character.
- Fixed a problem where DynComp would hang on the Mac
- Calls to clone are now correctly handled.
Documentation
- Indicated that a NoSuchMethodException will be generated if a method
in the JDK that could not be instrumented is called.
A new format for declaration records in Daikon trace data was introduced. The AnnotateNullable tool was released. A number of bugs were fixed.
User-visible changes
Daikon supports a new format for declaration records. This format
allows front ends more flexibility and an increased ability to use
arbitrary variable names. The program point hierarchy and relationships
between variables are explicitly stated in their declarations rather
than being inferred from variable names. See Appendix A of the
user manual for more information.
User-visible changes
Creates the new declaration format by default.
AnnotateNullable determines which variables in a Java program were ever null during execution. Its primary use is for performing inference for a type system that detects null dereference errors. An example is the Nullness Checker that is part of the Checker Framework (see https://checkerframework.org/manual/#nullness-checker/). See section "AnnotateNullable" of the Daikon user manual for more information.
User-visible changes
Enhanced the build of dcomp_rt.jar to limit expected error messages and
make clear if any unexpected problems were encountered in the build.
Bug-fixes
Fixed a problem with clone where the instrumentation incorrectly added a
call to a instrumented version of clone where it did not exist.
Fixed some problems with the instrumentation of equals.
Support new declaration format
Daikon was enhanced to better support program points that are basic blocks. Also, some minor enhancements and bugs fixes were made and the documentation was improved.
Bug fixes
Permit guarding invariants (the left-hand-sides of implications) to be
EltNonZero as well as NonZero invariants, to accommodate guarded
invariants over array contents.
Create better error messages when declaration records for
expected enclosing variables for arrays are not present.
User-visible changes
Added IsPointer invariant. The IsPointer invariant is true if
the corresponding variable only takes on legitimate pointer
values (in an x86 executable). IsPointer is disabled by default
Added support for program points that are basic blocks. Using
variables at the basic block level allows intra-procedural
invariants (such as loop invariants) to be found. There is
also support for combining multiple basic blocks into a single
program points so that invariants can be found over variables from
different basic blocks. See the configuration option
daikon.FileIO.merge_basic_blocks for more information.
Added the configuration option daikon.ProglangType.convert_to_signed
(default false). If true, 32 bit values whose high bit is on, are
treated as negative numbers.
Documentation
The differences between a minimal and complete installation are
better explained. The installation instructions are improved.
A section on removing irrelevant output was added.
A section on using Eclipse for editing the Daikon source was added.
DynComp (Java) was enhanced with a number of new options. It has a new significantly faster mode where it only tracks references (and not primitives). It also has additional output that makes it easier to determine where interactions occurred.
User-visible changes
DynComp can now be directed, with the --no-primitives switch, to
only track the comparability of object references, i.e. it will
ignore primitive values. DynComp runs significantly faster when
only tracking references.
DynComp has a number of new command line options that provide
information on the source of the interactions that merge variables.
Bug fixes
The JUnit tests can now be run directly from the jar file. All
necessary input files are resources in the jar file and the unit test
code handles them as resources.
A number of problems with building Daikon on Windows were resolved. Daikon now builds correctly with Cygwin. The installation and build instructions were updated.
Bug fixes and minor enhancements were made to Daikon, Kvasir, and DynComp (Java). The "repair" output format is no longer supported by Daikon.
User-visible changes
Eliminated support for the "repair" output format. We are not aware of
users who are still utilizing this format; let us know if you are.
Bug fixes
Enhanced mainHelper (the programmatic interface to Daikon) so that
it can be called multiple times. This allows a caller to process
multiple unrelated trace files within a single run.
Bug fixes
When giving the hashcode values of function parameters, previous
versions of Kvasir sometimes used an internal pointer value. Kvasir
now correctly uses the address on the program's stack instead. Since
Daikon doesn't infer many invariants over hashcode values, the only
visible effect is that the presence or absence of "<reference value>
has only one value" invariants is more consistent.
Bug fixes
Calling the superclass equals method (i.e. super.equals(Object))
resulted in an infinite loop. This has been fixed.
The clone method of Object is now instrumented.
Bug fixes and minor enhancements were made to Kvasir, DynComp (Java), DynComp (binary) and Daikon.
Bug fixes
A memory leak in Kvasir's handling of variable names has been
fixed.
Portability
An unneeded directory "auxprogs" whose presence caused a build
failure on some systems has been removed.
Bug fixes
DynComp's treatment of "argc", "argv", and the environment pointer
"environ" now works consistently across different versions of the
C library.
The previous version of DynComp would crash if a 64-bit program
attempted to access memory at too large a virtual address, which
happened on systems with certain security options enabled. The
range of supported addresses has been increased to 1TB, which is
the maximum practical with the current data structure, and
overflows are now caught with an error message.
Bug fixes
The equals method of Object is now instrumented. (The manual
incorrectly claimed that this was the case in version 4.3.0.)
User-visible changes
Added the daikon.PrintInvariants.print_filtered configuration option.
When set to true all invariants that would have been filtered out
are printed along with the matching filter.
Added the daikon.Daikon.show_stack_trace configuration option. When
set to true, a stack trace will be printed for user/input errors that
terminate Daikon prematurely. Under normal circumstances, Daikon
just prints an informative error message when such an error occurs.
The input file and line number are printed when an incorrectly formatted
program point name is encountered in a trace file.
Bug Fixes
Fixed a bug (reported by Radu Vanciu) where Daikon crashed when
printing simplify output on some OneOfSequence invariants on a
subsequence with a lower bound.
A new tool (DynComp) calculates variable comparability information for Java programs. Kvasir has been enhanced to support x86-64 Linux platforms.
Bug fixes
Distributed .jar and .class files are now runnable on a Java 5 (aka
Java 1.5) JVM, rather than requiring Java 6.
Portability
Kvasir now runs on x86-64/Linux platforms: i.e., AMD64 and Intel
64 (aka EM64T or IA32e) processors running Linux in 64-bit mode.
We have copied into Kvasir a fix from the Valgrind development
tree to allow Kvasir to compile on systems where gcc uses
-fstack-protector by default, such as some recent Ubuntu
systems. (The symptom of the problem is a linking failure
mentioning "__stack_chk_fail".)
The DynComp tool for Java programs is available in this release. This tool performs dynamic type inference to determine which variables should (and should not) be compared to one another when inferring invariants. It can make Daikon run faster and avoid generating irrelevant invariants. See section 7.2 of the manual for more information.
This is a maintenance release with few substantive changes.
Bug fixes
A bug that occurred when Daikon.jar appeared twice in the classpath
on windows was fixed.
User-visible changes
Error messages are more informative.
Configuration-variable-related Error messages were improved. Two bugs in Annotate, and one in the utilMDE utility package, were fixed. The source code was made compatible with Java 6.
User-visible changes
Error messages caused by bad configuration variables have been improved.
Bug fixes
A GCD (greatest common divisor) routine has been fixes so that it
does not infinite-loop when called on (infinity, -infinity).
The Annotate tool, which inserts Daikon output in source code (as
stylized comments) has been restructured to fix two problems.
Annotate now handles nested classes, and it recognizes (some)
variables that Daikon intentionally omits. These problems
previously caused Annotate to issue a warning of the form
Warning: Annotate: Daikon knows nothing about field ...
which means that Annotate found a variable in the source code that was
not processed by Daikon.
Implementation changes
Daikon now compiles cleanly when using Java 6. (Java 6's compiler
issues more warning messages than Java 5's compiler does.)
A new mode was added to Daikon that allows it to handle constants more efficiently. Also, a new configuration option was added and one was renamed.
User-visible changes
Daikon can now optionally ignore static constant variables during
processing (saving space and time) and include the names of those
constants in the output of sample dependent invariants (such
as OneOf, LowerBound, and UpperBound). For example, if the
UpperBound invariant 'i < 1024' is found and a constant 'bufsize'
with the value 1024 exists, the invariant will be printed as
'i < bufsize'. This mode is controlled by the configuration option
daikon.PrintInvariants.static_const_infer. It is not enabled by
default.
Normally, if a method exit is executed without a preceding enter,
Daikon exits with an error. If the new configuration option
daikon.FileIO.ignore_missing_enter is set to true, the unmatched exits
will be ignored instead. This can make it easier to process parts
of a dtrace file.
The configuration option daikon.Daikon.disable_derived_variables was
renamed to daikon.derive.Derivation.disable_derived_variables
A server mode was added to Daikon. Two new command line switches were added to InvariantChecker to more finely control what invariants are checked.
User-visible changes
Added a switch (--conf) that checks only invariants that are above
the default confidence level.
Added a switch (--filter) that checks only invariants that are not
filtered by the default filters.
User-visible changes
Added a server mode for daikon (specified by the --server switch).
In this mode, Daikon processes files that are placed in the specified
server directory until a filename that ends in ".end" is encountered.
InvariantChecker was enhanced to handle multiple input files and count the violations for each file. Some minor enhancements and bugs fixes were made to Daikon.
User-visible changes
Added a switch (--dir) that will apply all of the samples in any
dtrace files in the specified directory to all of the invariant
files in the directory. The number of samples that violated an invariant
are reported for each invariant file.
Only invariants above the default confidence level and that have
not been filtered out by the default filters are checked.
User-visible changes
Modified the simplify format of some invariants so that 'i' is used
as a free variable rather than 'a'.
Bug fixes
The windows daikonenv.bat script was fixed to correctly handle
paths with blanks in the directory names
The percentage progress information was fixed to work on dtrace
files specified with full pathnames.
Some enhancements and bug fixes were made to Daikon. Repeated declarations are no longer an error. A new invariant and derived variable were added.
User-visible changes
Multiple declarations of a program point are now allowed if they
are identical to the previous declaration. This makes it easier
to operate on multiple trace files.
Added an invariant (PrintableString) that is true if each character
in a string is printable. PrintableString is not enabled by default.
Added a derived variable (StringLength) that represents the length
of a string. StringLength is not enabled by default.
Post variables in JML output are marked as "\new" rather than generating
a warning.
Bug Fixes
Simplify output now correctly references the length of synthetic
arrays such as a[].getClass().
Some enhancements and bug fixes were made to Daikon. Programs with a large number of variables are handled more efficiently. A number of configuration options were changed. PrintInvariants supports a new command line option.
User-visible changes
Suppression processing in Daikon has been optimized. It will
process program points with a large number of variables more
efficiently. The configuration options related to suppression
have been changed. See the documentation for details.
Added support for the --ppt-select-pattern command line option to
PrintInvariant.
By default, Daikon no longer replaces post variables with orig
variables that have the same values. The old behavior can be
obtained by using the configuration option remove_post_vars.
Bug fixes
Previously, some information used to determine whether or not a
variable needed to be guarded was sometimes incorrect. This
resulted in both unnecessary and missing guarding. This has
been fixed.
Bugs were fixed in Chicory, Kvasir, and Daikon. Chicory was enhanced to correctly instrument programs that use an incompatible version of BCEL and to not instrument unselected classes. Kvasir was modified to avoid making calls to the system C library. Using the system C library can cause problems on some versions of Linux.
Chicory uses the Byte Code Engineering Library (BCEL) to instrument class files. Errors can occur if the application uses an incompatible version of BCEL. Chicory has been modified to identify and load its copy of BCEL when multiple copies of BCEL are in the class path. It will also issue a warning if multiple copies of BCEL are in the class path and the application version is not the first one. This behavior can be overridden with the default_bcel command line option
Chicory only modifies classes that are instrumented. Previous versions made unnecessary changes to uninstrumented classes.
The configuration option "omit_hashcode_values_Simplify" now uses artificial values for hashcodes that should remain consistent from run to run rather than omitting the invariant altogether.
A problem where Daikon crashed when producing JML output was fixed.
Kvasir has changed to use internal versions of some C standard library routines, and versions provided by Valgrind, rather than linking with the system's C library. This avoids an initialization problem that caused Kvasir to crash on systems whose system library used thread-local storage (such as some recent Fedora Core systems), improves portability, and conforms to the best-practice suggested by the Valgrind maintainers.
The only known user-visible effect is that some floating-point values are now printed differently in the last digit because of rounding differences. The value printed generally still corresponds to the same internal representation, but the difference can be visible in Daikon's output for values of type "float", because Daikon represents them internally with type "double".
This is a maintenance release with few substantive changes.
Performance changes
Non-instantiating suppression processing has been optimized to
run 5 to 15% faster.
Minor enhancements were made to Chicory, Daikon, and Kvasir. Chicory more accurately determines whether or not a class is a boot (system) class. Daikon better handles spreadsheet data. Kvasir's DynComp option more consistently handles array references.
User-visible changes
Changed the mechanism by which boot (system/jdk) classes are
determined (boot classes are not instrumented and errors will
occur if they are instrumented mistakenly). Previously the name
of the class was used. Now if the class loader is null (which
indicates the boot class loader), the class is presumed to be a
boot class. Also added a command line option (boot_classes) that
can specify a regular expression that determines what classes are
considered to be boot classes.
User-visible changes
Daikon prints a warning message if it encounters non-standard
program point names in a trace file and the --nohierarchy
switch is not used. This change is irrelevant for most users,
since, for trace files corresponding to an execution of a program,
such as those obtained from Chicory and Kvasir, the --nohierarchy
switch should not be used. For trace files obtained from
spreadsheet data, such as from a csv file using convertcsv.pl,
the --nohierarchy switch should be used.
The divides invariant (b % a == 0) is redundant and thus not printed
when a linear binary invariant of the form 'C*a = b' exists and C
is an integer constant.
User-visible changes
DynComp's treatment of indexed memory accesses, local variables,
and position-independent library code has been modified to be more
consistent. The most noticeable change is that base pointers and
indexes used in array dereferences are now always counted as
interacting.
This is a maintenance release with few substantive changes.
User-visible changes
Daikon no longer uses the JDKDIR and DAIKONPARENT environment
variables.
The examples section of the Daikon manual has been slightly
streamlined, and several small typos have been fixed.
The examples subdirectory of the distribution has been re-organized:
the Java examples have been put in a "java-examples" directory, and the
"kvasir-examples" directory has been renamed to "c-examples".
Daikon no longer prints "Creating implications", which is
irrelevant to most users.
User-visible changes
New command-line option --array-length-limit has been added.
Some enhancements were made to Daikon. The list of modified and unmodified variables in DBC and JML output is more accurate. A configuration option was added to control the method by which Daikon determines variable comparability. And the treatment of values near zero with fuzzy comparisons has been changed.
User-visible changes
Changed the way that modified/unmodified variables are determined
in DBC and JML output. The new version uses equality invariants
between pre and post variables to provide more complete information.
Added daikon.VarInfo.declared_type_comparability configuration option.
By default, Daikon only considers variables declared with the same
type name to be comparable. If this option is set to false, Daikon
does not consider the type name in determining comparability.
Floating point values are subject to roundoff errors so Daikon
compares them with a "fuzzy" rather than exact test. Previously
the test always used a relative comparison. Under this approach a
floating point value of 0.0 was only equal to exactly 0.0. This
test has been changed so that values closer to zero than the fuzzy
ratio squared will also be considered equal to 0.0. The fuzzy
ratio is set via the configuration option daikon.Invariant.fuzzy_ratio
Bug Fixes
Fixed a bug in the Simplify formatting of index comparison invariants
that occurred on slices starting from non-zero indices.
This is a bug-fix release. Several bugs in Daikon were fixed.
User-visible changes
Fixed bugs in the LinearTernaryFloat and LinearBinaryFloat
invariants such that the coefficients and constants of these
invariants print out as decimals rather than integers.
Bug Fixes
Fixed an error in LinearTernary invariant that showed up when
merging LinearTernary invariant that formed lines rather than
planes.
Fixed a problem in the equality set optimization that caused
variables with NaN values to show up as equal (Java considers a
NaN value to be unequal to everything, including itself or another
NaN value).
Fixed InvariantChecker so that it works correctly with trace files
that contain declaration records.
This is a bug-fix release. It also adds a new, more detailed mode to the x86 DynComp tool.
User-visible changes
Changed the default value of configuration parameter
daikon.PptRelation.enable_object_user from "true" to "false".
User-visible changes
Fixed bugs in operation of --purity-file and in --omit-var
switches.
User-visible changes
Added a --dyncomp-detailed-mode command-line option to provide
more detailed (accurate) but slower DynComp variable comparability
analysis.
Implementation changes
Ported Kvasir to use a recent development version of Valgrind
3.2.0 from the Feb. 10, 2006 snapshot of the Subversion
repository.
Enhancements were made to the Chicory and Kvasir front ends. Chicory allows a regular expression to choose variables to be omitted by name and has some new and modified command line options. Kvasir has some new command line options to better control its comparability analysis.
User-visible changes
The --omit-var <regex> command line option was added. Variables whose
name matches the regular expression will be omitted from the trace file.
The option --daikon-args must be used to specify any arguments to
daikon when it is automatically run with the --daikon or --daikon-online
options. The --daikon and --daikon-online options no longer accept
an argument
The option --trace-percent has been removed and replaced with the
--sample_start option. The --sample_start option starts sampling after
the specified number of samples have been recorded. The sampling
percentage decreases as more samples are recorded.
The option --comparability-file was added to specify a decl
formatted file with comparability information.
Static variables are only included once at each program point. Static
variables are named with their full static pathname (for example:
package.class.varname) rather than their relative name (this.varname)
User-visible changes
Added several command-line options (--dyncomp-units,
--dyncomp-dataflow-only, --dyncomp-dataflow-comp) to provide
finer user control over the DynComp comparability analysis tool,
which is distributed along with Kvasir.
Enhancements were made to the Mangel-Wurzel and Kvasir front ends. Mangel-Wurzel better supports arrays, C++, and regular expressions for specifying program point names. Some Kvasir command line options were updated.
Enhancements
The Windows version now includes full support for regular expression
matching in --ppt-omit-pattern and --ppt-select-pattern command-line
options. The --dtrace-gzip option is also now fully supported.
Sending dtrace output to stdout now works.
Output for statically-sized, multidimensional arrays is now supported.
There are new command-line options --flatten-arrays,
--max-flatten-array-size, and --max-array-size to control how arrays
are output.
Bug fixes
Some minor bugs in array output have been fixed.
C++ support has been better tested, with bug fixes added for reference
parameters and return values, and proper scoping of exit PPT processing
with respect to binding and destruction of block-scope variables.
Code with multiple return statements on the same line no longer results
in duplicate exit PPT names.
User-visible changes
The --limit-static-vars command line option was removed. The default
behavior now only outputs static variables at program points for
the file that contains the static variable. The new option
--all-static-vars outputs static variables at all program points.
Daikon's support for C and C++ has been substantially improved. The Mangel-Wurzel C/C++ front end now runs on Windows, and it supports new option --ignore-system-structs. The Kvasir C/C++ front end has greatly improved support for C++, it supports a new pointer type coercion feature, and it makes use of the new Fjalar dynamic instrumentation framework.
The Purity Analysis Kit can determine which methods of your program are pure observer methods, and so can be treated as derived variables. Many small improvements to Daikon's output have been made (but most users will only notice small changes to the output).
User-visible changes
The shell configuration files (daikon.bashrc, daikon.cshrc,
daikonenv.bat) do better checking of whether the user has set the
required configuration variables.
Errors in the Windows configuration file (daikonenv.bat) have been
corrected.
The default ("Daikon") output format has been made more Java-like.
As one example,
this.theArray.class == "java.lang.Object[]"
now prints as
this.theArray.getClass() == java.lang.Object[].class
Daikon's comparability tests, which determine what variables may
be compared to one another (and so may co-occur in an invariant)
have been improved.
Daikon outputs fewer logically redundant invariants. (For
instance, the tests that suppress, from the output, method
invariants when a stronger invariant occurs as an object
invariant, have been improved.)
Implementation detail
Guarding (controlled by the Daikon.guardNulls config option) has
been completely re-implemented.
The Daikon regression tests (not included in the distribution due
to size, but available on request) have been made easier to use.
In particular, they now require only two environment variables to
be set, and set all other environment variables appropriately.
Documentation changes
The installation instructions have been modified to reflect the
fact that the environment variable DAIKONDIR, rather than its
parent DAIKONPARENT, is the preferred setting for the user to
configure.
Bug fixes
Annotate can now locate all Daikon variables that correspond to
class fields. This improves the output and eliminates a warning
message.
User-visible changes
C++ support is greatly improved. New features include support
for inheritance (printing out superclass member variables),
reference parameter variables, member function declarations both
within and outside of class bodies, and more consistent naming of
C++ function and variable names (enabling proper handling of
OBJECT program points by Daikon).
Simplified the format of the program point list (ppt-list) files.
Added a pointer type coercion feature. A user can specify in a
.disambig file the actual type of a pointer with some other
declared type. This is useful for obtaining fields of pointers
that are declared as void*.
Implementation changes
Re-factored all of the Kvasir and DynComp code to use the Fjalar
framework. Fjalar is a C/C++ dynamic analysis framework. The
new directory structure reflects the separation between the
Fjalar framework and the Kvasir and DynComp tools that are built
upon the framework.
Documentation changes
The Daikon User Manual describes C++ support in more detail.
Enhancements
Mangel-Wurzel now runs on Microsoft Windows as a command-line utility
with the Microsoft Visual C/C++ compiler. (Mangel-Wurzel does not
support GCC on this platform.)
Some minor changes have been made to the way Mangel-Wurzel looks for
include files and libraries.
There is a new command-line option, --ignore-system-structs, to ignore
fields of structs defined in system include files. (Typically, ordinary
users have no need to examine the internals of structures like FILE that
are defined as interfaces to the underlying operating system.)
User-visible changes
The command line option --avoid-static-recursion was removed. Chicory
will now traverse the static fields of a give class at most once by
default.
The trace file now contains the contents of the --ppt-select-pattern
and --ppt-omit-pattern switches as comments near the end of the file.
Chicory issues a warning if the result of the settings for the
--ppt-omit-pattern and --ppt-select-pattern switches don't match any
program points. It also complains if no records are printed to the
trace file (which can happen even if some methods match if those methods
are never executed)
The Purity Analysis Kit computes which methods of a Java program are pure (have no externally visible side effects). The Purity Analysis Kit now includes a command-line option, --daikon-purity-file, that causes it to write a file that is appropriate for passing to Chicory via its --purity-file option. The Purity Analysis Kit was written by Alexandru Salcianu and is available from http://www.mit.edu/~salcianu/purity/.
Enhancements were made to the Kvasir, Mangel-Wurzel and Chicory front ends. Kvasir and Mangel-Wurzel both handle arrays of structures and pointers better than previously. The command line options for Chicory were standardized. The documentation of each was reorganized and updated. Daikon has some new and enhanced configuration options.
User-visible changes
Config option "Daikon.noInvariantGuarding" has been renamed to
"Daikon.guardNulls", and instead of being a boolean, is a
string with three possible values: "always", "never", or "missing".
See the documentation for details.
Added daikon.inv.unary.sequence.SingleSequence.SeqIndexDisableAll
configuration option to disable all of the SeqIndex invariants
(SeqIndexIntEqual, SeqIndexFloatLessThan, etc).
Added DerivedVariableFilter that will filter out invariants that
use a specific class of derived variable. See the configuration
option daikon.inv.filter.DerivedVariableFilter.class_re for more
information.
Bug fixes
Fixed a bug (reported by Christoph Csallner) where Chicory crashed
when the --std-vis (now std-visibility) switch was used and a field
was accessed in a non-instrumented class (in this case an
interface).
Enhancements
Chicory's switches were renamed for consistency as follows:
--configs is now --config-dir
--heap_size is now --heap-size
--std-vis is now --std-visibility
--watch-static-recursion is now --avoid-static-recursion
The --trace-percent switch now takes a floating point argument
The documentation was also updated to provide a better explanation
of the switches.
Enhancements
Implemented a more robust data structure traversal mechanism
that can better handle dereferencing pointer fields inside of
arrays and arrays of structures.
Documentation changes
Re-organized and updated the Kvasir section in the Daikon User
Manual. Updated examples, added categories for command-line
options, and added a section describing the DynComp dynamic
comparability analysis tool that comes with Kvasir.
Bug fixes
Fixed a bug that was causing wurzel to crash when processing switch
statements followed by an implicit return.
Enhancements
Some of the mangel configuration options have changed to make it
easier to set up at installation time. Most options now get their
defaults from reading an options file instead of through environment
variables. See the Daikon manual for details.
There are new command-line options for mangel to directly specify
strict ANSI, gcc, and Microsoft compatibility modes.
Instrumented programs now run much faster due to improvements in the
Mangel-Wurzel runtime.
Arrays of structs are now treated as arrays of each scalar struct field
(instead of being ignored), as in the other Daikon front ends.
A number of bug fixes and minor enhancements have been made to the Mangel-Wurzel, Kvasir, and Chicory front ends. The older front ends dfec and dfej have been removed from the distribution.
Printing of string variable values has been fixed to do a better job of distinguishing between null-terminated strings, and arrays of arbitrary byte values or pointers to a single character object.
Bug fixes
A memory allocation problem that caused Kvasir to crash in some
Linux environments, including Red Hat version 9, has been worked
around. To catch such problems more quickly in the future, we now
regularly test Kvasir on four Linux distribution versions.
Added support for giving names to unnamed struct/union/enum types
and fixed bugs that prevented Kvasir from traversing into
certain structs within large programs with many files which include
the definitions of those structs.
Improved the garbage collector for DynComp comparability analysis
to allow it to scale up to larger programs.
Manual
The description of program point names and variable names has been
improved, consolidating several different discussions and clarifying
the interpretation of arrays.
Implementation detail
The Daikon code no longer uses any raw generic types. All uses of
generic types (such as List) are supplied a type parameter. When
compiled using the supplied Makefile, there are no "javac -Xlint"
warnings.
Added command line options --trace-percent (only output the specified percentage of program points) and --watch-static-recursion (only output a particular static once).
We have reduced the size of the Daikon distribution by removing several un-needed or out-of-date components.
Eclipse plug-in
The Eclipse plug-in is no longer being maintained, so it has been
removed from the manual. We hope to re-include this when the plug-in
gets updated again.
dfec
Dfec has been removed from the Daikon distribution and the manual. To
run Daikon on C/C++ programs, we use Kvasir (for Linux/x86) or
Mangel-Wurzel (for all other platforms).
dfej
Dfej has been removed from the Daikon distribution and the manual. to
run Daikon on Java programs, use Chicory.
Ajax
The Ajax package for computing comparability of variables in Java
programs has been removed from the distribution and the manual. It
only works with Java 1.1 and is the bottleneck in running dfej. A
replacement is in testing and will be included in a future release.
A new source-based C/C++ front end, Mangel-Wurzel, is now available. Mangel-Wurzel uses Rational Purify to determine the validity and extent of pointers. A license for Purify is required. The initial version is available only for Linux/86, but future versions are planned for Windows and possibly other platforms. Kvasir will remain the suggested C/C++ front end for Linux/86.
More information is available in the 'Mangel-Wurzel' section of the Daikon User Manual.
Bug fixes
Optimized initialization code to greatly reduce start-up time when
running Kvasir on large programs.
Kvasir and Chicory have been enhanced with new command line options, improved performance and documentation. Kvasir can more efficiently trace a subset of a program. Chicory supports pure functions as additional Daikon variables. Also, Daikon problems are now tracked in a Bugzilla database.
Daikon problems are now tracked in the Bugzilla database at at: http://pag.csail.mit.edu/bugzilla/. There are separate products for Daikon and Kvasir. Problems with Chicory and other front ends should be submitted against the Daikon product.
User Changes
Daikon runs on Mac OS (the Apple Macintosh). This is not due to a
change in Daikon, but because Apple has finally released a Java 1.5
JVM.
Bug fixes
Fixed several bugs in Annotate, the program that inserts Daikon's
output into source code as comments. This eliminates errors reported
by the JML syntax checker (available at https://www.cs.ucf.edu/~leavens/JML/).
User changes:
The values of static variables in classes that are not initialized
are no longer included in the trace file. Instead, the trace file
notes them as nonsensical until the class is initialized.
Added the --purity-file=<file> switch. Chicory will read <file>
for pure methods (methods which do not induce side effects). It
will then invoke these methods, using their return values as
normal variables. That is, if a class has variables int a, b, c,
and pure method int x(), then Chicory will produce variables a,b,c
and x() for Objects of this type.
Added --std-vis switch. When on, Chicory will only traverse fields which
are visible from a given program point. For instance, a program point from
class A will not include private fields from class B.
Added --heap_size switch to specify the maximum heap size of the target
program.
See the Chicory section of the Daikon user manual for more information.
Bug Fixes
Overriding methods that return a subtype of the original method no
longer produce duplicate decl information.
Arrays of objects with String fields are now handled correctly.
Documentation changes:
Documented --premain switch to Chicory. Noted that the default output file
for Chicory is . (not ./daikon-output).
User changes:
The selective program point and variable tracing functionality
(--ppt-list-file and --var-list-file options, respectively) now
work more efficiently and reliably than before, and can integrate
with the pointer type disambiguation functionality (--disambig).
Grant the user the ability to comment-out lines in the program point
and variable list files by placing a '#' character at the beginning
of lines.
Added a --smart-disambig option to allow Kvasir to heuristically
infer pointer type information when generating a disambiguation file.
Documentation Changes
Added "Tracing only part of a program" and "Using pointer type
disambiguation with partial program tracing" entries to the Kvasir
section of the Daikon User Manual.
The dynamic comparability analysis in Kvasir has been improved (it indicates which variables interact with one another). Switch --var-select-pattern has been added to Daikon, and a variety of bugs have been fixed and enhancements performed.
User changes:
Added new switch --var-select-pattern for symmetry with
--var-omit-pattern. Daikon produces output only for variables whose
names match the regular expression.
Configuration option daikon.FileIO.unmatched_procedure_entries_quiet
defaults to false, and its output has been made more concise.
Improved Daikon's diagnostics that indicate it was provided no program
points, variables, or samples.
User changes:
The DynComp variable comparability analysis tool (invoked by using
the --with-dyncomp option) generates much more precise
comparability sets.
The --dyncomp-fast-mode command-line option makes DynComp run
faster and use less memory at the expense of slightly less
precision (by adjusting the handling of manifest literals).
Added a tag garbage collector to DynComp, to avoid running out of
memory on larger programs. The --no-dyncomp-gc option turns off
the garbage collector, and the --gc-num-tags=N option tells
DynComp to garbage collect after every N tags have been assigned
(default is 5,000,000). If your program still runs out of memory
while running Kvasir with DynComp, try the --dyncomp-fast-mode
option.
Kvasir can now produce variable comparability information, Chicory can now run Daikon online (without writing any files to disk), and the new DtraceDiff program can be used to compare Daikon trace files.
User changes:
New --with-dyncomp option adds variable comparability information
to .decls files. Variable comparability information indicates
which variables should (and should not) be compared to one another
when inferring invariants; it can make Daikon run faster and avoid
generating irrelevant invariants. This option may be used with
the --decls-only option to generate a .decls file without a
.dtrace file.
Implementation changes:
Kvasir now uses a development version of Valgrind 3.0 instead of
the release version of Valgrind 2.2. This should have no
user-visible effects.
User changes:
Added --daikon-online option. Behavior is similar to that of the
--daikon option, but instead of writing and reading back a dtrace
file, Chicory and Daikon communicate directly via a socket. This
can avoid creation of large temporary .dtrace files on disk, and
can make Daikon run faster.
New:
This is a new utility to compare data trace (.dtrace) files using
a content-based, rather than text-based, comparison.
Invoke it like
java daikon.tools.DtraceDiff [DECLS1]... DTRACE1 [DECLS2]... DTRACE2
See the usage message or Daikon manual for information about
additional command-line options.
DtraceDiff stops by signalling an error when it finds a difference
between the two data trace files. (Once execution paths have
diverged, continuing to emit record-by-record differences is
likely to produce output that is far too voluminous to be useful.)
It also signals an error when it detects incompatible program
point declarations or when one file is shorter than the other.
Implementation changes:
Java-family formats now use reflection to access fields. This
makes it possible to access non-public fields. The Quant helper
methods do not throw exceptions when given illegal arguments.
Runtime-check instrumenter can emit "invariant-checker" classes.
This is primarily a maintenance release with bug fixes to Kvasir and Chicory.
User changes:
Added --bit-level-precision command-line option for more accurate
output of variables involved in bit-level operations.
Bug fixes:
Kvasir achieves better accuracy because it is now able to find
arrays and other structs nested within structs (which are local
and global variables) and only prints out initialized data within
arrays.
Bug fixes:
Chicory no longer changes the order in which classes are initialized.
User changes:
Because of their size, the C examples for dfec are no longer included
in the distribution. Examples for Kvasir (the recommended C front end)
are still available.
Daikon now supports C++: it is possible to infer invariants over C++ programs, using the Kvasir front end. (Kvasir works on Linux/x86 systems.) As usual, many bugs have been corrected, and in particular, Kvasir has been made much more robust. The Daikon manual has been copy-edited and reorganized for clarity.
User changes
When using the --ppt-select-pattern option to Chicory, it is no longer
necessary to write two regular expressions, one of which matches the
class and another of which matches the procedure. This makes the
option more consistent with similar argument to other parts of the
toolset, and with the --ppt-omit-pattern argument.
Documentation changes
The Daikon manual has been cleaned up and copy-edited (e.g., for
consistent use of punctuation and typographical conventions). A few
sections have been reorganized, and some redundant material has been
eliminated. These changes should make the manual more readable.
User changes
In order to reduce the amount of extraneous output, added heuristics
to avoid dereferencing pointers to certain types of variables
(such as FILE*) associated with the C library and operating
system which are unlikely to be interesting for the user.
Added C++ support:
Features:
Kvasir outputs the member variables of C++ classes just like those
within C structs, generates :::OBJECT and :::CLASS invariants,
performs C++ name demangling, treats member functions like regular
functions with an extra 'this' pointer parameter, and outputs
static class member variables.
Limitations:
Kvasir does not print the contents of classes defined in external
libraries. For example, Kvasir outputs the contents of a char*,
but not the contents of the C++ string class.
Kvasir ignores classes in which any member function definition
appears within the class body. Kvasir only produces output for
classes all of whose member function definitions appear outside the
class body.
Support for inheritance and polymorphic member function calls have
not yet been tested.
Bug fixes
Fixed a variety of segmentation faults in Kvasir. Kvasir now runs on
programs of significant size (for example, gcc 3.4.3, which is over
300,000 lines of code).
This version includes significant improvements to the manual, enhancements to Kvasir, and bug fixes. Version 3.1.10 of the Daikon plug-in for Eclipse is also now available.
Documentation changes
The Daikon manual has been improved in the following ways:
* Two new sections in "Troubleshooting" chapter: "Too much output" and
"No samples".
* Kvasir (C front end) section has been restructured for clarity.
* Descriptions of file formats have been clarified.
The instrumentation (front end) sections of the Daikon Developer
Manual have been expanded, and in particular a new section about how
to instrument C programs has been added.
Bug Fixes
Kvasir now compiles on older versions of gcc such as 2.96.
User changes
The manual includes a new section "minimal installation": users who
want to detect invariants only in Java programs merely need to put
daikon.jar on their class path.
By default, Daikon creates .inv.gz files containing a serialized
representation of the invariants. Previously, you had to specify the
-o flag. You can still specify -o to override the default name.
Developer changes
The developer manual discusses issues related to calling System.exit().
dfej
User changes
Ajax is disabled by default. You can control it with the --ajax and
--no-ajax flags.
dfej creates compressed trace files (.dtrace.gz) by default. You can
still explicitly specify the name of the trace file.
Documentation changes
Documented that environment variable DTRACELIMITTERMINATE causes an
exception to be thrown when the .dtrace file reaches the specified
size; it does not forcibly terminate the program.
User changes
Changed behavior of environment variable DTRACELIMITTERMINATE to cause
an exception to be thrown when the .dtrace file reaches the specified
size, rather than forcibly terminating the program.
Bug fixes
Correct a problem with classes that are not in a package; Chicory
previously created invalid program point names for the constructors of
such programs.
Correct a problem with outputting values of type "char".
The manual has been restructured and simplified, in order to clarify that the Chicory and Kvasir front ends (for Java and C, respectively) are preferred over the older dfej and dfec front ends.
A number of problems with the Chicory instrumenter were fixed. In particular, files necessary to run Chicory (when not running from source) were added to the distribution.
Configuration option daikon.FileIO.unmatched_procedure_entries_quiet is now true by default.
Invariants over typeOf derived variables are disabled in the instrumenter and Annotate's output.
User Changes
Kvasir now produces all of its output (both variable declarations and
run-time values) in one .dtrace file instead of as separate .decls and
.dtrace files. The --decls-file=<filename> command-line option forces
Kvasir to generate separate .decls and .dtrace files, as before.
Bug Fixes
Several refinements which produce better output for arrays and structs
when using pointer type disambiguation. Also fixed some bugs, making
Kvasir more robust across different Linux platforms (kernel and gcc
version differences).
Version 3.1.10 of the Daikon plug-in for Eclipse (written by David Cok) has been released. It is compatible with Daikon version 3.1.7 (which is included with the plug-in), but with dfej version 4 (which can be downloaded from the Daikon webpage). A version of the plug-in that is fully compatible with Daikon 4 is still in preparation.
The 4.0.0 version of Daikon introduces many substantial enhancements. These improvements include:
- Liberalized license permits unrestricted use.
- New Java class file front end ("Chicory") handles Java 5.0 (and earlier).
- Annotation and other source manipulation components handle Java 5.0.
- New Eclipse plug-in eases running many components of the Daikon system.
- New runtime checking tool can insert assertions into your programs.
- Command-line options have been standardized across Daikon components.
- Many bug fixes, documentation updates, and other minor improvements.
Daikon's licensing terms have been liberalized. Daikon is now distributed without restrictions under an MIT/BSD-style license.
Chicory is a new Daikon front end for Java. Its functionality is very similar to that of the dfej tool, and it supports most of the same command-line options. However, Chicory has three substantial advantages over dfej:
- Chicory is much easier to use: when running your Java program, just replace the "java" command with "java daikon.Chicory". For instance, if you usually run java mypackage.MyClass arg1 arg2 arg3 then instead you would run java daikon.Chicory mypackage.MyClass arg1 arg2 arg3 That's all there is to it! Note that Chicory does not require you to perform separate instrumentation or compilation steps, as dfej does. Furthermore, a single command can both create trace files and run Daikon: java daikon.Chicory --daikon mypackage.MyClass arg1 arg2 arg3 See the Daikon manual for more options.
- Chicory supports all versions of Java, including Java 5.0. By contrast, dfej only supports Java 1.4 and earlier.
- Chicory is platform-independent (and requires no special action to build), since it is written in Java.
Daikon is now accompanied by an Eclipse plug-in (written by David Cok) that provides the functionality of instrumenting files, obtaining trace information, analyzing those traces, and creating appropriately annotated Java source code. The plug-in works with Eclipse version 3.0.1 and later. You can find documentation for the plug-in at http://pag.csail.mit.edu/daikon/doc/daikonHelp.html . The 3.1.7 version of the plug-in supports versions of Daikon up to Daikon 3.1.7 and (like Eclipse 3.0.1) only versions of Java up to Java 1.4.2. A version of the plug-in for Eclipse 3.1 and Daikon 4.0.0 is forthcoming.
User changes
Daikon now permits program point declarations (which previously
appeared only in .decls files) to appear in the .dtrace file as well.
Each declaration must appear either in a .decls file or in a .dtrace
file, not in both, and any declaration in a .dtrace file must precede
all samples for that program point. This feature allows incremental
processing of .dtrace files for languages such as Java that support
dynamic linking. As part of this change, it is now required that
:::ENTER program points be declared before corresponding :::EXIT
program points so that the set of original variables are available when
processing exit point declarations.
The generation of implications has been modified. If Daikon finds
multiple invariants with identical run-time truth values, one is chosen
as a predicate and used for all of the implications. For example,
suppose that all of the following implications are true, where the
letters stand for invariants:
A <=> B
A => C
A => D
B => C
B => D
Previously, Daikon would print all of these implications. Now, it
prints only the first three, since the last two are redundant and can
be inferred from the first three.
The following command-line options have been renamed, for consistency
with other components of the Daikon distribution.
OLD NEW
--ppt RE --ppt-select-pattern=RE
--ppt_omit RE --ppt-omit-pattern=RE
--var_omit RE --var-omit-pattern=RE
Developer changes
Daikon's source code is now written in Java version 5.0. This means
that you will need a Java 5 compiler to compile Daikon, and you will
need a Java 5 JVM to run Daikon. (You may be able to run Daikon on an
older JVM by using a utility like retroweaver:
http://retroweaver.sourceforge.net/ .)
dfej
The dfej front end for Java continues to support only Java 1.4 and earlier. You can run dfej's output on any JVM, but dfej takes as input a Java 1.4 (or earlier) program.
dfej outputs more variables; in particular, you may notice slightly more "foo.class" variables that give the run-time type of variable foo.
The following command-line options have been renamed, for consistency with other components of the Daikon distribution. OLD NEW -daikon_debug --debug -daikon_depth= --nesting-depth= +daikon_instrument --instrument -daikon_instrument --no-instrument +daikon_listclosure --linked-lists -daikon_listclosure --no-linked-lists +daikon_exceptions --exceptions -daikon_exceptions --no-exceptions -daikon_includeonly=/RE/ --ppt-select-pattern=RE -daikon_omit=/RE/ --ppt-omit-pattern=RE -noajax --no-ajax -tracefilename= --dtrace-file= -declsfiledir= --decls-dir= -declsfiledirflat= --decls-flat --decls-dir= -instrsourcedir= --instr-dir=
Annotate and other components of Daikon (including runtimechecker, described below) handle Java 5.0 code. They continue to support all earlier versions of Java as well.
Annotate respects tabs in the source file. Previously, Annotate converted tabs to spaces.
A runtime-check instrumenter (named "runtimechecker") has been added to Daikon. The instrumenter creates a new version of Java source code; the modified version checks invariants as the program executes. For more details, see the "tools" section in the Daikon manual.
The runtime-check instrumenter may be useful for external tools. It is used, for example, by the Eclat tool (which is not a part of Daikon itself). Eclat automatically creates test cases that are much more likely than random to reveal errors in programs. You can download Eclat from http://pag.csail.mit.edu/eclat/ .
User Changes
Added a command-line option, --limit-static-vars, to limit the output
of static variables.
Added pointer-type disambiguation (--disambig and --disambig-file
options), which permits users to specify whether pointers are printed
as single elements or arrays.
Kvasir does not yet support C++. If support for C++ is important to
you, please send email to daikon-developers@lists.csail.mit.edu.
Bug Fixes
Numerous bug fixes result in Kvasir producing more accurate output,
most exposed only by obscure test cases.
dfepl
The following command-line options have been renamed, for consistency with other components of the Daikon distribution. OLD NEW --reference-depth= --nesting-depth= --dtrace-basedir= --dtrace-dir= --decls-basedir= --decls-dir= --instr-basedir= --instr-dir=
This version includes some improvements to the website, documentation enhancements and several bug fixes.
Documentation Changes
The Daikon publications webpage has been reorganized to bring all of
the publications relating to Daikon together on a single webpage.
Links have been added to other tools that perform dynamic invariant
detection. See http://plse.cs.washington.edu/daikon/pubs/.
The list of configuration options in the user manual was reorganized
to group the options by category.
Bug Fixes
An incorrect assertion that caused Daikon to fail on some inputs
was fixed. Some other minor problems were resolved as well.
User Changes
Daikon now has improved support for reading trace data from the
standard input or a named pipe. Together with the enhancement to
the Kvasir C front end allowing writing to a pipe, this removes the
need for an intermediate trace file, allowing Daikon to operate on
larger or longer-running programs. For more details, see
the "Reading trace data on the fly" section of the manual.
The printing filters were simplified and configuration
options were added to enable/disable each filter. See the
"Invariant Filters" and "List of Configuration Options" sections
of the manual for more information. Filter configuration
options are named 'daikon.inv.filter.<filter>.enabled'.
The user manual was enhanced with a section ('Loop invariants')
that describes how to find specific loop invariants if desired.
The configuration option 'daikon.FileIO.dtrace_line_count' was
added. This option allows the number of lines in the dtrace
file to be specified and avoids the overhead of having Daikon
counting them.
Daikon no longer uses the libraries jarkarta-oro.jar and log4j.
The mechanism for compiling splitter files was improved.
The process is more reliable, error messages are more
meaningful and the names of related configuration options
were changed. The option that selects the compiler to use is
'daikon.split.SplitterFactory.compiler' and the option that sets
the compiler timeout is 'daikon.split.SplitterFactory.compile_timeout'.
Developer Changes
Sections were added to the developer manual explaining regression
testing and how to analyze historical versions of Daikon.
Bug Fixes
A bug that could cause errors in programs that used variables
named "ps", "depth", or "prefix" was fixed.
User Changes
Kvasir now supports writing to a pipe. Used with Daikon's new
support for reading from a pipe, this removes the need for an
intermediate trace file, allowing Daikon to operate on larger or
longer-running programs. For more details, see the "Reading trace
data on the fly" section of the manual.
The Kvasir C front end now supports a number of command line options
for controlling what output is produced and where it is written. See
the "Kvasir options" section of the user manual for a list.
Bug Fixes
A number of bugs in Kvasir have been fixed, including one that
accidentally reduced the number of program points it output, and
another that caused arrays to have too many elements. On the
whole, Kvasir produces significantly more output than before.
User Changes
When two or more variables are always equal, any invariant that is
true over one variable is true over all of the variables. Daikon
prints invariants only over one variable (the leader) from the
equal set. The algorithm used for choosing the leader has been
improved. A variable that is less derived is chosen ahead of one
that is more derived. Variables derived from parameters are
chosen last. And other things being equal, the variable with the
least complex name is chosen first.
Two new options were added. The --list_type option specifies
information to be added to the "ListImplementors" section of the
.decls file. The --mem_stat option prints memory usage statistics
info a file named "stat.out" in the current directory. The
"Command line options for Daikon" section of the users manual
was also reorganized to be more clear.
The configuration option "Daikon.disable_derived_variables" was
added. Derived variables will not be created if this option is set to
true. See the "List of Configuration Options" section of the user
manual for more information.
Bug Fixes
Two bugs were fixed in the LinearTernary invariant. Under some
conditions, LinearTernary invariants were reported when there were
samples that did not fit. Also, coefficients too large for an
integer were printed incorrectly.
Developer Changes
Daikon warns if you (incorrectly) use "String" in a .decls file,
as a representation type synonym for "java.lang.String". The use
of "String[]" was and continues to be an error, but now gives a
more specific message. The C front ends dfec (distributed
separately) and Kvasir have been updated accordingly.
User Changes
The dynamic C front end Kvasir has been extensively improved. It
is now based on the stable 2.2.0 release of Valgrind, fixing
failures on some Linux distributions. Global variables are now
instrumented, and there is some support for outputting array
values. Changes have been made to allow instrumenting C programs
compiled with a C++ compiler (work to support C++ itself is
ongoing). Two incompatibilities with previous versions of Kvasir
should be noted: the format of global function names has changed,
for consistency with the new names for global variables, and
Kvasir may now produce much more output for a given program run.
Developer Changes
Kvasir now uses "java.lang.String" rather than "String" as the
representation type for strings in .decls files (see "Daikon
Developer Changes" in this file).
Developer Changes
Dfec now uses "java.lang.String" rather than "String" as the
representation type for strings in .decls files (see "Daikon
Developer Changes" in this file).
Bug Fixes
An incompatibility between dfepl, the Perl front end, and versions
of Perl starting with 5.8.1 has been fixed. Dfepl has been
verified to work with Perl version 5.8.4.
User Changes
Added new script trace-add-nonces.pl, which adds nonces to a
.dtrace file. Nonces associate a procedure exit with a procedure
entry, and some parts of Daikon's toolset require .dtrace files to
contain nonces.
Changed the way that output formats are specified to the Daikon, PrintInvariants, and Annotate tools. Previously, one supplied arguments such as --java_output, --jml_output, etc. Now, one uses --format NAME, where name is the name of the output format. The formats are Daikon, DBC, ESC, IOA, Java, JML, Simplify, and repair. See the "Invariant syntax" section of the user manual for more information. The user manual was also updated with improved descriptions of the output formats.
LinearBinary invariants are now printed in standard form (ax + by + c = 0) rather than slope intercept form, (y = ax + b). They also now have integer coefficients and like LinearTernary invariants, the coefficient of the x variable is positive.
Improved portability to Windows systems by changing instances of the literal "\n" in code to System.getProperty("line.separator"), or using println().
Removed most calls to System.exit in Daikon. This makes it easier to call methods (including main) defined by Daikon programmatically.
The "--no_reflection" and "--max_invariants_pp N" options were added to Annotate tool. See the "Annotate tool" section of the user manual for more information.
The Annotate class was made public so that it could be accessed programmatically from other Java applications. State-holding static variables were removed from Annotate, so that multiple calls of main() from within another application always yield the same initial Annotate state.
Support for a number of deprecated optimizations was removed. The global program point hierarchy optimization, the top-down approach to optimizing the program point / variable hierarchy, and linked suppressions were removed along with their corresponding configuration options.
The Range invariants (EqualMinusOne, EqualOne, EqualZero, GreaterEqual64, GreaterEqualZero, BooleanVal, Bound0_63, Even, and PowerOfTwo) are now checked on elements of arrays in addition to scalar variables. These are not normally visible (since they are implied by the Bound and OneOf invariants), but are used internally to suppress other invariants.
Added the configuration option daikon.PptRelation.enable_object_user. See the "List of Configuration Options" section of the user manual for more information.
The mechanism by which invariants are instantiated was simplified. See the "New Invariants" section of the developer manual for more information.
The Kvasir dynamic C front-end has undergone a number of internal improvements, in preparation for adding support for global variables and arrays. The only user-visible changes so far are minor improvements in finding the names of structure members and the correct locations of function parameters in some circumstances.
Several bugs in the LinearyTernary invariant were fixed. Under some conditions, LinearTernary invariants were missed when initial points formed a line and not a plane. Also, the canonical form of the coefficients were changed to be more readable.
A bug in non-instantiating suppressions was fixed. The problem occurred when multiple distinct negative values were used to specify in the decl file that a variable was comparable to all other variables.
Added configuration options daikon.Daikon.undo_opts and daikon.Daikon.quiet, See the "List of Configuration Options" section of the user manual for more information.
The non-instantiating suppression mechanism has been significantly optimized. Performance for programs with large number of variables should be significantly enhanced. Configuration option daikon.suppress.NIS.antecedent_method now defaults to true.
The PrintInvariants utility was upgraded to handle InvMap files (the output from the diff utility) as well PptMap files. The command line option --config was added so that PrintInvariants can read files of configuration options.
The command line option --java_output was added to the Annotate utility. See the "Annotate" section of the user manual for more information.
Added configuration options daikon.FileIO.continue_after_file_exception and daikon.PrintInvariants.print_all. See the "List of Configuration Options" section of the user manual for more information.
Added MemberString invariant (looks for strings that appear in a sequence of strings) and comparison invariants between two sequences of strings (SeqSeqStringEqual, SeqSeqStringGreaterThan, SeqSeqStringGreaterEqual, SeqSeqStringLessThan, and SeqSeqStringLessEqual).
Removed the StringComparison invariant. This invariant was previously replaced by the individual invariants StringEqual, StringLessThan, StringLessEqual, StringGreaterThan, and StringGreaterEqual but still remained in the documentation and code.
The implementation of SubSequence and SubSequenceFloat invariants has been changed to create separate invariants for SubSequence and SuperSequence. This should have no user visible ramifications except that the configuration options to enable SuperSequence invariants have names that are distinct from the SubSequence invariants (SuperSequence, and SuperSequenceFloat). See the "List of Configuration Options" section of the user manual for more information. These invariants are also documented in the "Invariant List" section of the user manual.
The internal mechanism for adding invariants has been changed. The variable specific factories have been replaced with a single list of invariants. See the "New Invariants" section of the developer manual for more information.
Modified Java formatting to use FuzzyFloat comparisons rather than directly comparing floating point numbers. By default, FuzzyFloat comparisons are used when generating invariants. More information on fuzzy comparisons is available in the 'List of configuration options' section of the user manual under the configuration option daikon.inv.Invariant.fuzzy_ratio.
Fixed some minor bugs in the Java formatting that allow them to compile more cleanly.
Added NonZeroFloat invariant.
The kmeans clustering program now compiles under gcc 3; previously, it only compiled under gcc 2. (kmeans can be used to create splitting conditions via AI clustering; see section 'Cluster analysis for splitters' in the manual.)
We have moved the Daikon mailing lists (daikon-announce, daikon-discuss, and daikon-developers) from pag.csail.mit.edu to lists.csail.mit.edu. Any changes to your subscription must be made at lists.csail.mit.edu.
Daikon now includes a new front-end for C programs, named "Kvasir". Unlike previous C front-ends, which worked by rewriting source code, Kvasir uses the Valgrind framework and debugging information in the DWARF-2 format to trace a program's execution given only a binary. Kvasir is generally easier to use, faster and more robust than the old C front-end, but it does not yet support all of the features of the old C front-end, and it can be used only on x86 platforms running Linux. More information on Kvasir is in the "Binary C front end Kvasir" section of the user manual
Several bugs in Daikon's JML output were fixed. The JML output is now parsed correctly by both the JML tools and ESC/Java2. (However, the "assignable" clause is given a default value; it will be made more accurate in a future release.)
Added Annotate as a replacement for MergeEsc. Annotate inserts Daikon-generated invariants into Java source files as ESC/JML/DBC annotations. See the "Annotate" section of the user manual for more information.
Added InvariantChecker as a replacement for MakeInvariantChecker. InvariantChecker checks invariants against data trace files. InvariantChecker resolves a number of limitations in MakeInvariantChecker. See the "InvariantChecker" section of the user manual for more information.
The java output format has been significantly enhanced. See the --java_output entry in the Daikon "Command line options" section of the user manual for more information.
Some of the dfej command line options have changed. See the "dfej options" section of the user manual for more information.
Added the configuration option daikon.FileIO.unmatched_procedure_entries_quiet See the "List of Configuration Options" section of the user manual for more information.
Some bugs were fixed based on user feedback. Daikon will no longer terminate with an error if the trace file ends in the middle of the record. The last record will simply be ignored. The dtype-perl script is now included in the distribution.
A new optimization was added to Daikon to suppress invariants that are implied by other invariants. Suppressed invariants are neither printed nor written to the invariant output file. This optimization reduces memory use and limits the number of redundant invariants that are printed. It can be disabled if desired via the daikon.suppress.NIS.enabled configuration variable. See the "List of Configuration Options" section of the user manual for more information.
Added the TraceSelect program which creates random selection of data for splitters. See the "Random selection for splitters" section of the user manual for more information.
The output that is printed while daikon is running was enhanced to show the percentage of the trace file that has been processed. The configuration variables daikon.FileIO.count_lines and daikon.FileIO.max_line_number control this feature. See the "List of Configuration Options" section of the user manual for more information.
The manual was updated to explain how to pass environment variables to an instrumented java program. See the "dfej options" section of the user manual for more information.
The manual was updated to explain how to work-around the use of realloc in C programs. See the "C program requirements" section of the user manual for more information.
The environment variables DTRACELIMIT and DTRACELIMITTERMINATE were added to dfej. These allow the size of the output tracefile to be controlled. See the "dfej options" section of the user manual for more information.
Fixed some bugs in dfej, dfec, and MergeESC.
The implementation of sequence index comparison invariants has been changed to create separate invariants for each comparison (Equal, NonEqual, LessThan etc). This should have no user visible ramifications except that the configuration options to enable these invariants have new names. See the "List of Configuration Options" section of the user manual for more information. These invariants are also documented in the "Invariant List" section of the user manual.
The user manual has been updated. The "C examples" section has been improved; a subsection on "Dealing with large examples" has been added. The "C program requirements" and "No return from procedure" sections were also updated.
The developer manual has been updated with a new "Unit Testing" section.
Three new binary invariants were added to Daikon: square, bitwise subset, and divides without remainder. Each of these is checked both between scalar variables and also between the corresponding elements of a sequence. For more information, see the "Invariant List" section of the user manual.
The configuration variable for enabling the BitwiseComplement invariant is now a member of the type specific Numeric class rather than of the type specific FunctionUnary class. See the "Configuration options" section of the user manual for details.
The configuration variable daikon.Daikon.use_suppression_optimization (default true) was added. This controls whether or not invariants that are implied by other invariants are suppressed. See the "Configuration options" section of the user manual for details.
The command line option '--omit_from_output [0rs]' was added to Daikon. This option controls what invariants are written to the output invariant file. It is possible to remove program points that are not referenced in the trace file, reflexive invariants, and invariants that are suppressed. See the "Command line options" section of the manual for more information.
Daikon version 3 is now the standard distribution.
Daikon version 2 reads an entire data trace file into memory and then processes it in multiple passes. By contrast, Daikon version 3 processes samples incrementally in a single pass, without needing to store the entire trace file in memory. This allows version 3 to handle data trace files of essentially unlimited size. There are a number of other differences between version 2 and version 3. The most important are summarized below.
-
A number of command line options have changed. The options noInvariantGuarding and suppressSplitterErrors are now configuration variable. The options suppress_cont, no_suppress_cont, and suppress_post have been removed. The option prob_limit has been replaced by the similar option conf_limit. The track option was added for debugging specific invariants.
-
There are many new configuration variables. For details, see the "Configuration options" section of the manual.
-
You may get slightly different output from that of version 2. The two versions test the same invariants, but the two versions use different optimizations, and the mechanism for calculating the statistical confidence level of each invariant has changed. As a result, which invariants are printed can differ between the two versions. For example, version 3 prints some redundant invariants that are not printed in version 2. These changes are mainly minor; they do not affect output correctness, only verbosity; and they will become less as more optimizations are added to version 3.
New command-line options have been added to the LogicalCompare program. See the manual for details.
The developers manual has been significantly rewritten for clarity and some sections have been added.
The default VarComparability has been changed from none to implicit. Decls file may need to be changed to specify the comparability as 'none' at the top of the file if implicit is not the appropriate default.
Some minor changes were made to the user and developer manuals to enhance clarity.
A number of bugs were fixed, particularly in Daikon version 3 (experimental).
Fixed some Simplify formatting bugs.
Fixed some dfej bugs.
The implementation of SubSet and SuperSet invariants has been changed to create separate invariants for SubSet and SuperSet. This should have no user visible ramifications except that the configuration options to enable SuperSet invariants have names which are distinct from the SubSet invariants (SuperSet, and SuperSetFloat). See the "List of Configuration Options" section of the user manual for more information. These invariants are also documented in the "Invariant List" section of the user manual.
Added the LogicalCompare program which compares two sets of invariants describing a software module and determines if one set of the invariants implies the other. See the "LogicalCompare" section of the user manual for more information.
Added the daikon command line option --disc_reason that will indicate the reason a specified invariant was not printed. See the "Command line options for Daikon" section of the user manual for more information
Added configuration options daikon.simplify.Session.trace_input, and daikon.simplify.LemmaStack.synchronous_errors to provide additional information when debugging Simplify problems. See the "List of Configuration Options" section of the user manual for more information.
Both the user manual and developer manual have been significantly enhanced. The sections concerning the C and Java front ends in the user manual have had significant troubleshooting information added. The dfec (C front end) section also makes more clear that dfec only supports programs that are BOTH legal ANSI/ISO C programs and legal C++ programs.
The implementation of Sequence-Scalar, Sequence-Sequence and Pairwise comparisons has been changed to create separate invariants for each possible comparison (<, <=, ==, >=, >). This should have no user visible ramifications except that the configuration options to disable comparisons have individual names (e.g., SeqFloatEqual, SeqFloatGreaterEqual, etc). See the "List of Configuration Options" section of the user manual for more information. These invariants are also documented in the "Invariant List" section of the user manual.
Daikon now requires JDK 1.4. If you are still using JDK 1.3, you will need to upgrade in order to run Daikon.
Added a developer manual (developer.html, developer.info, developer.pdf, etc) to the doc directory. The developer manual indicates how to extend Daikon with new invariants, new derived variables, and front ends for new languages. It also contains information about implementation and debugging. The user manual has been simplified by moving appropriate sections to the developer manual.
Added the MakeInvariantChecker program (in V3 only) which can take a set of invariants found by Daikon and create a specialized checking program that checks only those invariants. See the "Invariant Checker" section of the manual for more information.
Changed the default for Simplify iterations from 1000000 to 1000. This should provide reasonable results while being less likely to take an inordinate amount of time. Also added the configuration options daikon.simplify.Session.simplify_timeout and daikon.simplify.Session.verbose_progress. See the "List of Configuration Options" section of the manual for more information.
Added new command line options for daikon.pl (--instrument, --nogui, --src, and --debug). See the "Command line options for daikon.pl" section of the manual for more information.
The internal mechanism for formatting output has been enhanced. There is now a single routine (format_using (OutputFormat)) that replaces the previous output specific format routines. See the "New formatting for invariants" section of the manual for more information on adding new formatting routines.
Added the capability to use a decls file to the convertcsv.pl script. See the usage message of convertcsv.pl for more information.
The perl front end (dfepl) has been significantly enhanced. An additional Perl example has been added. See the "Perl examples" and "Instrumenting Perl programs" sections of the manual for more information.
The manual has been reformatted and edited in a number of areas to improve clarity and readability.
Floating-point quantities can be considered equal even if they differ slightly (say, due to floating-point roundoff). Configuration option daikon.inv.Invariant.fuzzy_ratio sets the ratio by which floating-point numbers may differ and still be considered equal; a value of 0 disables these approximate comparisons.
A new front end for csv (comma-separated-value) files is provided; run program convertcsv.pl, which appears in the bin/ directory.
The manual now contains a list of all invariants that Daikon detects, with a short description of each. Recall that users can add their own (possibly domain-specific) invariants.
Other parts of the manual have been enhanced, such as descriptions of variable names and dealing with too-large datasets.
"Dummy invariants" permit properties that are not in Daikon's grammar to be output, when they appear as splitting conditions. It is possible to specify in the splitter info file how to format such properties in each of the output formats that Daikon supports.
The manual describes how to deal with contradictory invariants, which Daikon might sometimes produce due to a bug or a limitation.
dfec now works with gcc 2.96 (the version that is distributed with Red Hat Linux, but which is not an official gcc release).
The Context GUI bug that caused it to sometimes print question marks in invariants is fixed.
dfej now produces output with program points named in Java, not JVML format: "foo(int, java.lang.String[])", not "foo(I[Ljava/lang/String;)".
Fix several bugs, mostly reported by Tao Xie.
There are two improvements to running Daikon under Windows. First, Cygwin is no longer necessary to run Daikon: the daikonenv.bat file sets up the Windows environment to permit Daikon to be run without Cygwin. Second, when running under Cygwin, the cygwin-runner.pl script smooths over differences in path conventions between Cygwin and Windows.
Daikon can detect invariants in Perl programs. See the "Perl examples" and "Instrumenting Perl programs" sections of the manual.
Three new mailing lists have been set up: daikon-announce@lists.csail.mit.edu daikon-discuss@lists.csail.mit.edu daikon-developers@lists.csail.mit.edu To subscribe, visit http://lists.csail.mit.edu/mailman/listinfo.
The Context GUI now shares the same look and feel as the Tree GUI. Furthermore, .dci files are no longer necessary for the Context GUI, and its setup has been somewhat simplified.
The --no_suppress_cont option to Daikon and to PrintInvariants displays invariants even if they are implied by controlling program points.
The -y option to Diff includes (statistically) unjustified invariants.
To customize the behavior of the C runtime system (for instance, to produce gzipped .dtrace files or to customize the runtime's behavior when it detects a memory error in your program), edit file $DAIKONDIR/front-end/c/daikon_runtime.h.
The manual sections on dealing with variable comparability, large .dtrace files, and memory exhaustion have been revised and expanded.
Improved directions for building dfec (if you have a license to the EDG C/C++ front end). dfec has also been updated to use EDG 3.0 instead of EDG 2.45. dfec is substantially more robust; most C programs and many C++ programs should be instrumented without difficulty.
Fixed a small problem in the example sections of the manual.
Explained a JTB ParseException error and how to work around it.
Version 2.3.17 (9 October 2002)
Version numbers were wrong in last release; re-release to fix the problem.
Manual improvements: note that local variables are not examined; that Daikon can work over data that comes from sources other than program executions; that all exit points must have the same number of variables; that "nonsensical" is permitted as a value in a .dtrace file.
Bugfix release.
Discontinued the compiled distribution; now there is only one Daikon distribution, the source distribution, which includes both pre-compiled files and source files.
Added top-level Makefile, which simplifies Daikon installation.
dfec enhancements: added --flatten-mdas option improved documentation of disambiguation file
CreateSpinfoC program creates splitting conditions via static analysis of C programs; this complements CreateSpinfo, which works for Java programs.
daikon_runtime.h lists many customization variables for the Daikon C Runtime.
Fix bug when running from daikon.jar.
Improvements to detection of floating-point invariants.
Manual gives example of use of orig variables, explains what to do when Daikon runs slowly, discusses Ajax "too many levels of symbolic links" error.
Daikon reports invariants over floating-point numbers. Previously, it silently ignored floating-point numbers.
The runcluster.pl program performs cluster analysis (a machine learning technique) to produce splitter info files. This is in addition to other ways of producing splitter info files, such as static analysis or writing them by hand.
The .decls file format now supports auxiliary information for declared types. It can indicate that a collection never contains duplicates or that order does not matter (both useful for avoiding obvious invariants over sets), properties of null in a collection, and whether a variable is a call-by-value parameter (and so can never change, from the point of view of the caller). Use of this information reduces Daikon's output.
The manual emphasizes that dfec only works on ANSI/ISO C programs (that are also legal C++ programs), and gives a number of hints for making your C programs compliant.
Bugfix release.
Improve dfec documentation: explain more error messages (including array bounds errors), add gcc installation instructions, explain uninitialized array element processing.
This release coordinates with a new release of the dfec binaries (at http://pag.csail.mit.edu/daikon/download/).
Remove some innocuous syntax anachronisms from example C programs. Add the example C programs to the distribution. Add manual section describing the example C programs. Improve dfec documentation in the manual. The Context GUI now supports C programs.
Rearrange distribution to avoid very long file names in tar file.
Rewrite of dfec documentation. dfec is now easier to use, more robust, and supports new options, such as struct instrumentation depth.
Remove incorrect dfej documentation for "-instrsourcedir=.".
Add documentation for CreateSpinfo program.
Add new configuration options daikon.split.FileCompiler.compiler and daikon.split.TimedProcess.compile_wait.
MergeESC tool inserts Daikon output into Java source files as ESC/Java comments.
Invariant Diff can compute set difference, union, and xor. It can produce output in the new InvMap format, and can read that format. New flags enable specification of custom comparators.
dfej's "-daikon-omit" flag can be a regular expression.
Daikon takes a --config_option flag to specify configuration settings.
Ajax tool bug fixes.
Improved installation and troubleshooting instructions.
Add --files_from command-line argument to Daikon.
Add -a and -l command-line arguments to Diff.
Add four new programs to the distribution: createspinfo.pl trace-untruncate trace-purge-fns.pl trace-purge-vars.pl
Manual enhancements:
- Add section on configuration options.
- Add paragraph about debugging options.
- Add text about two new GUI filters.
- Typo fixes.
Add new flags to Diff program.
Manual enhancements:
- Fix errors with "-noajax" flag in manual.
- Describe redundant invariants and how to print them.
- Explain format of Java program point names.
- Explain more invariant (Daikon output) syntax.
- Discuss dealing with errors in the external Ajax and Simplify programs.
Support for splitter files that specify conditions to use when detecting implications (conditional invariants).
Daikon's --config option permits reading and saving sets of configuration options.
The Daikon Java runtime respects the DTRACEAPPEND environment variable.
dfec requires that gcc be present.
Added Context GUI, which shows relevant invariants in a separate window as you browse code in a text editor.
Added many index entries to manual.
Added linear ternary invariants, of the form z = ax + by + c.