History of Daikon changes ========================= 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 as `daikon.html` or `daikon.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 as `developer.html` or `developer.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 javadoc` It is also available at http://plse.cs.washington.edu/daikon/download/api/ . Version 5.8.22 (June 3, 2025) ============================= All Daikon tools now work with Java 8-24. Bug fixes: * fixed Daikon issues 515, 532, 536 and 556 * fixed Fjalar issues 66 and 68 Version 5.8.20 (May 14, 2024) ============================= 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) Version 5.8.18 (June 23, 2023) ============================== Support Rocky Linux. All Daikon tools now work with Java 20. Version 5.8.16 (Nov 9, 2022) ============================ All Daikon tools now work with Java 18. Fixed a bug in DynComp's command-line processing. Version 5.8.14 (October 6, 2022) ================================ 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) Version 5.8.12 (July 14, 2022) ============================== 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). Version 5.8.10 (November 1, 2021) ================================= 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). Version 5.8.8 (March 2, 2021) ============================= Added DynComp `--dump` option, which dumps instrumented classes to a file. Improved DynComp comparability results for JDK 11. Version 5.8.6 (December 2, 2020) ================================ 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. Version 5.8.4 (July 22, 2020) ============================= 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. Version 5.8.2 (May 4, 2020) =========================== Improved installation instructions. Updated Valgrind from 3.14.0 to 3.15.0. Version 5.8.0 (April 14, 2020) ============================== 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. Version 5.7.2 (November 7, 2018) ================================ 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). Version 5.7.0 (August 22, 2018) =============================== 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. Version 5.6.6 (July 2, 2018) ============================ DynComp: - Fix issue #129 - Too many parameters for an annotation method. Fjalar/Kvasir: - Fix issue #27 - Incorrect categorization of some SIMD instructions. Version 5.6.4 (April 3, 2018) ============================= 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. Version 5.6.2 (February 2, 2018) ================================ 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. Version 5.6.0 (December 4, 2017) ================================ 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. Version 5.5.14 (October 3, 2017) ================================ 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. Version 5.5.12 (September 5, 2017) ================================== Chicory: - Improve support for programs with multiple threads. Fjalar/Kvasir: - We updated the underlying Binutils infrastructure to version 2.28.1. - Fix issue #10 Version 5.5.10 (July 4, 2017) ============================= Chicory and DynComp: - Refactored some instrumentation code. Includes a few bug fixes. Version 5.5.8 (June 2, 2017) ============================ DynComp: - Fixed a few DynComp bugs. Version 5.5.6 (May 2, 2017) =========================== DynComp: - Fixed a few DynComp bugs. Kvasir: - We updated the underlying Binutils infrastructure to version 2.27.0. Version 5.5.4 (April 3, 2017) ============================= 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. Version 5.5.2 (March 1, 2017) ============================= 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. Version 5.5.0 (February 1, 2017) ================================ Kvasir: - The option `--with-dyncomp` has been changed to `--dyncomp` and is now the default. Use `--no-dyncomp` to not run the DynComp portion of Kvasir. - Clarified instructions for building the sample Fjalar tool. DynComp: - The `--compare-sets-file` option has been renamed to `--comparability-file`. - The `--trace-sets-file` option has been renamed to `--trace-file`. - The `--no-cset-file` option has been removed, this is now the default. - The `--no-jdk` option has been removed, use `--rt-file=NONE` instead. Documentation: - Improved discussion of DynComp and comparability sets. Version 5.4.6 (January 3, 2017) =============================== 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. Version 5.4.4 (December 2, 2016) ================================ - 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. Version 5.4.2 (November 3, 2016) ================================ Fixed numerous DynComp bugs. Version 5.4.0 (October 4, 2016) =============================== 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. Version 5.3.10 (September 1, 2016) ================================== 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` Version 5.3.8 (August 1, 2016) ============================== Improved portability: * support g++ 6.1 * support Fedora 23 * support newer version of jdk8 Miscellaneous bug fixes and minor improvements. Version 5.3.6 (July 5, 2016) ============================ 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. Version 5.3.4 (June 1, 2016) ============================ Miscellaneous bug fixes and minor improvements. Version 5.3.2 (May 2, 2016) =========================== Daikon: - Command-line argument `--user-defined-invariant` makes Daikon compute a user-defined invariant in addition to those that are built in to Daikon. - Command-line argument `--disable-all-invariants` disables 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." Version 5.3.0 (April 5, 2016) ============================= 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. Version 5.2.26 (March 10, 2016) =============================== 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. Version 5.2.24 (March 4, 2016) ============================== Documentation: - Added more examples of invariants. - Improved instructions on building Daikon and Kvasir. Version 5.2.22 (February 1, 2016) ================================= 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. Version 5.2.20 (January 5, 2016) ================================ Documentation: - Improved instructions on building Daikon and Kvasir. Version 5.2.18 (December 5, 2015) ================================= 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. Version 5.2.16 (November 2, 2015) ================================= Chicory: - Improved handling of Java code containing synchronized locks. - Improved handling of Java initialization methods containing calls to other initialization methods. Daikon: - The `--shiny-print` option was renamed `--abridged-vars` to 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. Version 5.2.14 (October 5, 2015) ================================ Daikon: We have improved splitter verification testing. Documentation: Improved discussion of splitters Version 5.2.12 (September 3, 2015) ================================== Daikon: We have improved splitter file processing. Documentation: Improved discussion of splitters Version 5.2.10 (August 4, 2015) =============================== Chicory: - Modified generation of comparability values when using input from DynComp .decls file via `--comparability-file` option. 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. Version 5.2.8 (July 1, 2015) ============================ 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. Version 5.2.6 (June 2, 2015) ============================ 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 ``` Version 5.2.4 (May 1, 2015) =========================== 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 Version 5.2.2 (April 10, 2015) ============================== **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 Version 5.2.0 (March 3, 2015) ============================= 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. Version 5.1.16 (February 2, 2015) ================================= 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: https://github.com/codespecs/daikon/issues/37.) Updated bcel.jar (within plume.jar) for some minor improvements in JDK 8 support. Version 5.1.14 (December 22, 2014) ================================== 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) Version 5.1.12 (December 2, 2014) ================================= 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 Version 5.1.10 (October 31, 2014) ================================= 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. Version 5.1.8 (September 30, 2014) ================================== 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. Version 5.1.6 (August 29, 2014) =============================== 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: ```java private static final Boolean name = false; ``` Version 5.1.4 (July 31, 2014) ============================= Improved StackMap support. - for methods - for BASTORE instruction Improved Kvasir (C/C++ Daikon front end) support for 32bit hosts. Version 5.1.2 (June 30, 2014) ============================= 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. Version 5.1.0 (May 30, 2014) ============================ 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.) Version 5.0.8 (May 2, 2014) =========================== **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 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: https://github.com/codespecs/daikon/issues/10 https://github.com/codespecs/daikon/issues/29 https://github.com/codespecs/daikon/issues/30 Version 5.0.6 (March 28, 2014) ============================== **Daikon:** This release contains a fix for Daikon issue #28. See: https://github.com/codespecs/daikon/issues/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. Version 5.0.4 (February 28, 2014) ================================= **Daikon:** This release contains a fix for Daikon issue #27. See: https://github.com/codespecs/daikon/issues/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. Version 5.0.2 (January 31, 2014) ================================ **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). Version 5.0.0 (January 3, 2014) =============================== **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: https://github.com/codespecs/daikon/issues/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. Version 4.7.5 (December 12, 2013) ================================= * 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. Version 4.7.3 (November 1, 2013) ================================ * Fix for stack map problem in Chicory. Version 4.7.1 (October 8, 2013) =============================== * 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. Version 4.6.4 (June 23 2010) ============================ 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. Chicory ------- Documented Chicory options `--boot-classes=REGEX`, `--linked-lists`. Kvasir ------ **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. DynComp ------- Fixed a bug when searching for dcomp_premain.jar. The jar file will now be found if it is anywhere in the classpath. InvariantChecker ---------------- Added `--verbose` option that will print all samples that violate an invariant. Version 4.6.3 (December 18 2009) ================================ Kvasir's support for GCC 4.4 has been improved. Kvasir ------ **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. Version 4.6.2 (October 1 2009) ============================== Kvasir's support for x86-64 hosts and C++ programs has been improved. Kvasir ------ **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. Daikon ------ **User Documentation** Added an explanation of how additional data changes invariant output. Version 4.6.1 (September 1 2009) ================================ Support for GCC 4.3+ created binaries has been improved for Kvasir. Daikon ------ Documentation Appendix A (File Formats) of the Daikon user manual was moved to the developers manual. Kvasir ------ 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. Version 4.6.0 (July 1 2009) =========================== 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. Daikon ------ 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. Chicory ------- 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 Kvasir ------ 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. Version 4.5.5 (April 1 2009) ============================ Support for Daikon and DynComp for Java has been improved for Mac OS X. The Daikon user and developer manuals were enhanced. Daikon ------ 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. DynComp Java ------------ 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) Version 4.5.4 (February 2 2009) =============================== Bugs were fixed in Chicory and AnnotateNullable. Daikon's documentation was improved. Chicory ------- 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 Daikon ------ Documentation The Daikon user manual was improved with more detailed information on compiling Daikon, creating implications, and the information required with bug reports. AnnotateNullable ---------------- Bug fixes A null pointer exception that occurred in the case of the default package was fixed. Version 4.5.3 (January 2 2009) ============================== Resolved a number of problems in the build scripts and documentation for a complete Windows installation. Daikon ------ 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). Version 4.5.2 (December 1 2008) =============================== Some new String invariants were added to Daikon. 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) Version 4.5.1 (November 3 2008) =============================== 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. Daikon ------ 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. Version 4.5.0 (September 3 2008) ================================ Kvasir was updated to create the new format for declaration records. Kvasir was also upgraded to support newer versions of glibc. Kvasir ------ 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 Version 4.4.2 (August 1 2008) ============================= 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. Daikon ------ 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. Chicory ------- 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. Version 4.4.1 (July 1 2008) =========================== A number of bugs were fixed in Daikon, Chicory, and DynComp. The user manual was improved. Support for IOA format was removed from Daikon. 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. Chicory ------- Bug fixes - Fixed typo in comparability type when comparability information is included. DynComp ------- 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. Version 4.4.0 (June 11 2008) ============================ A new format for declaration records in Daikon trace data was introduced. The AnnotateNullable tool was released. A number of bugs were fixed. Daikon ------ 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. Chicory ------- User-visible changes Creates the new declaration format by default. AnnotateNullable ---------------- 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. DynComp ------- 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 Version 4.3.5 (April 3 2008) ============================ 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. Daikon ------ 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. Version 4.3.4 (December 1, 2007) ================================ 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. DynComp (Java) -------------- 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. Daikon ------ 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. Version 4.3.3 (October 3, 2007) =============================== A number of problems with building Daikon on Windows were resolved. Daikon now builds correctly with Cygwin. The installation and build instructions were updated. Version 4.3.2 (September 3, 2007) ================================= Bug fixes and minor enhancements were made to Daikon, Kvasir, and DynComp (Java). The "repair" output format is no longer supported by Daikon. 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. Kvasir ------ 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 " has only one value" invariants is more consistent. DynComp (Java) -------------- 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. Version 4.3.1 (August 2, 2007) ============================== Bug fixes and minor enhancements were made to Kvasir, DynComp (Java), DynComp (binary) and Daikon. Kvasir ------ 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. DynComp (Binary) ---------------- 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. DynComp (Java) -------------- Bug fixes The equals method of Object is now instrumented. (The manual incorrectly claimed that this was the case in version 4.3.0.) Daikon ------ 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. Version 4.3.0 (July 1, 2007) ============================ A new tool (DynComp) calculates variable comparability information for Java programs. Kvasir has been enhanced to support x86-64 Linux platforms. Daikon ------ Bug fixes Distributed .jar and .class files are now runnable on a Java 5 (aka Java 1.5) JVM, rather than requiring Java 6. Kvasir ------ 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".) DynComp Java ------------ 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. Version 4.2.16 (May 1, 2007) ============================ This is a maintenance release with few substantive changes. Daikon ------ Bug fixes A bug that occurred when Daikon.jar appeared twice in the classpath on windows was fixed. DtraceDiff ---------- User-visible changes Error messages are more informative. Version 4.2.15 (March 31, 2007) =============================== 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. Daikon ------ 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.) Version 4.2.14 (February 1, 2007) ================================= 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. Daikon ------ 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 Version 4.2.13 (January 1, 2007) ================================ A server mode was added to Daikon. Two new command line switches were added to InvariantChecker to more finely control what invariants are checked. InvariantChecker ---------------- 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. Daikon ------ 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. Version 4.2.12 (December 1, 2006) ================================= 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. InvariantChecker ---------------- 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. Daikon ------ 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. Version 4.2.11 (November 1, 2006) ================================= Some enhancements and bug fixes were made to Daikon. Repeated declarations are no longer an error. A new invariant and derived variable were added. Daikon ------ 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(). Version 4.2.10 (October 2, 2006) ================================ 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. Daikon ------ 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. Version 4.2.9 (September 1, 2006) ================================= 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 ------- 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. Daikon ------ 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 ------ 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". Version 4.2.8 (August 1, 2006) ============================== This is a maintenance release with few substantive changes. Daikon ------ Performance changes Non-instantiating suppression processing has been optimized to run 5 to 15% faster. Version 4.2.7 (July 1, 2006) ============================ 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. Chicory ------- 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. Daikon ------ 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. Kvasir ------ 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. Version 4.2.6 (June 1, 2006) ============================ This is a maintenance release with few substantive changes. Daikon ------ 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. Kvasir ------ User-visible changes New command-line option --array-length-limit has been added. Version 4.2.5 (May 1, 2006) =========================== 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. Daikon ------ 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. Version 4.2.4 (April 1, 2006) ============================= This is a bug-fix release. Several bugs in Daikon were fixed. Daikon ------ 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. Version 4.2.3 (March 1, 2006) ============================= This is a bug-fix release. It also adds a new, more detailed mode to the x86 DynComp tool. Daikon ------ User-visible changes Changed the default value of configuration parameter daikon.PptRelation.enable_object_user from "true" to "false". Chicory ------- User-visible changes Fixed bugs in operation of --purity-file and in --omit-var switches. Kvasir ------ 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. Version 4.2.2 (February 1, 2006) ================================ 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. Chicory ------- User-visible changes The --omit-var 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) Kvasir ------ 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. Version 4.2.1 (January 1, 2006) =============================== 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. Mangel-Wurzel ------------- 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. Kvasir ------ 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. Version 4.2.0 (December 6, 2005) ================================ 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). Daikon ------ 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. Annotate -------- Bug fixes Annotate can now locate all Daikon variables that correspond to class fields. This improves the output and eliminates a warning message. Kvasir ------ 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. Mangel-Wurzel ------------- 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.) Chicory ------- 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) Purity Analysis Kit ------------------- 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/. Version 4.1.7 (November 1 2005) =============================== 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. Daikon ------ 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. Chicory ------- 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. Kvasir ------ 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. Mangel-Wurzel ------------- 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. Version 4.1.6 (October 1 2005) ============================== 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. Mangel-Wurzel ------------- 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. Kvasir ------ 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. Daikon ------ 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. Chicory ------- Added command line options --trace-percent (only output the specified percentage of program points) and --watch-static-recursion (only output a particular static once). Removed components ------------------ 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. Version 4.1.5 (September 1 2005) ================================ 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. Mangel-Wurzel ------------- More information is available in the 'Mangel-Wurzel' section of the Daikon User Manual. Kvasir ------ Bug fixes Optimized initialization code to greatly reduce start-up time when running Kvasir on large programs. Version 4.1.4 (August 1 2005) ============================= 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. General ------- 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. Daikon ------ 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/). Chicory ------- 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= switch. Chicory will read 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). Kvasir ------ 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. Version 4.1.3 (July 1 2005) =========================== 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. Daikon ------ 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. Kvasir ------ 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. Version 4.1.2 (June 1 2005) =========================== 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. Kvasir ------ 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. Chicory ------- 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. DtraceDiff ---------- 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. Daikon ------ 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. Version 4.1.1 (May 1 2005) ========================== This is primarily a maintenance release with bug fixes to Kvasir and Chicory. Kvasir ------ 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. Chicory ------- Bug fixes: Chicory no longer changes the order in which classes are initialized. Dfec ---- 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. Version 4.1.0 (Apr 1 2005) ========================== 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. Daikon ------ 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. Kvasir ------ 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). Version 4.0.3 (Mar 1 2005) ========================== 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. Daikon ------ 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. Kvasir ------ Bug Fixes Kvasir now compiles on older versions of gcc such as 2.96. Version 4.0.2 (Feb 19 2005) =========================== Daikon ------ 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. Chicory ------- 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". Version 4.0.1 (Feb 13 2005) =========================== Daikon ------ 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. Kvasir ------ 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= 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). Eclipse plug-in --------------- 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. Version 4.0.0 (Feb 7 2005) ========================== 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. License ------- Daikon's licensing terms have been liberalized. Daikon is now distributed without restrictions under an MIT/BSD-style license. Chicory: class file-based front end for Java --------------------------------------------- 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. Eclipse plug-in --------------- 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. Daikon ------ 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 -------- 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. Runtime-check instrumenter -------------------------- 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/ . Kvasir ------ 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= Version 3.1.7 (Jan 1 2005) ========================== This version includes some improvements to the website, documentation enhancements and several bug fixes. Daikon ------ 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. Version 3.1.6 (Dec 1 2004) ========================== Daikon ------ 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..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. Dfej ---- Bug Fixes A bug that could cause errors in programs that used variables named "ps", "depth", or "prefix" was fixed. Kvasir ------ 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. Version 3.1.5 (Nov 1 2004) ========================== Daikon ------ 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. Kvasir (C front end) -------------------- 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). Dfec (C font end) ----------------- 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). Dfepl (Perl front end) ---------------------- 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. Scripts ------- 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. Version 3.1.4 (01 Oct 2004) =========================== 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. Version 3.1.3 (01 Sep 2004) =========================== 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. Version 3.1.2 (03 Aug 2004) =========================== 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. Version 3.1.1 (01 July 2004) ============================ 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. Version 3.1.0 (01 June 2004) ============================ 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.) Version 3.0.4 (01 May 2004) =========================== 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. Version 3.0.3 (01 April 2004) ============================= 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. Version 3.0.2 (27 February 2004) ================================ 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. Version 3.0.1 (02 February 2004) ================================ 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. Version 3.0.0 (19 December 2003) ================================ 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. Version 2.5.3 (01 October 2003) =============================== 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). Version 2.5.2 (03 September 2003) ================================= 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. Version 2.5.1 (01 August 2003) ============================== 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. Version 2.5.0 (01 July 2003) ============================ 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. Version 2.4.9 (02 June 2003) ============================ 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. Version 2.4.8 (13 May 2003) =========================== 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. Version 2.4.7 (30 April 2003) ============================= 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. Version 2.4.6 (24 April 2003) ============================= 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. Version 2.4.5 (1 April 2003) ============================ "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. Version 2.4.4 (2 March 2003) ============================ 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. Version 2.4.3 (1 February 2003) =============================== dfej now produces output with program points named in Java, not JVML format: "foo(int, java.lang.String[])", not "foo(I[Ljava/lang/String;)". Version 2.4.2 (20 January 2003) =============================== Fix several bugs, mostly reported by Tao Xie. Version 2.4.1 (1 January 2003) ============================== 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. Version 2.4.0 (1 December 2002) =============================== 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. Version 2.3.18 (2 November 2002) ================================ 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. Version 2.3.16 (1 October 2002) =============================== Bugfix release. Version 2.3.15 (12 September 2002) ================================== 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 Version 2.3.14 (1 August 2002) ============================== 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. Version 2.3.13 (17 July 2002) ============================= 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. Version 2.3.12 (11 July 2002) ============================= Daikon reports invariants over floating-point numbers. Previously, it silently ignored floating-point numbers. Version 2.3.11 (9 July 2002) ============================ 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. Version 2.3.10 (10 June 2002) ============================= Bugfix release. Version 2.3.9 (4 June 2002) =========================== Improve dfec documentation: explain more error messages (including array bounds errors), add gcc installation instructions, explain uninitialized array element processing. Version 2.3.8 (10 May 2002) =========================== 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. Version 2.3.7 (1 May 2002) ========================== 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. Version 2.3.6 (5 April 2002) ============================ 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. Version 2.3.5 (1 March 2002) ============================ Add --files_from command-line argument to Daikon. Add -a and -l command-line arguments to Diff. Version 2.3.4 (17 February 2002) ================================ 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. Version 2.3.3 (11 February 2002) ================================ 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. Version 2.3.2 (7 December 2001) =============================== 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. Version 2.3.1 (8 October 2001) ============================== 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. Version 2.3.0 (11 September 2001) ================================= Added linear ternary invariants, of the form z = ax + by + c.