C++TESK Testing ToolKit v1.0.16 has been released. The following things have been done.
- Bug leading to a segmentation fault on 64-bit systems has been fixed
- Improvement of the Eclipse IDE plugin has been done
- Macro CPPTESK_SET_TRACE_FILE(file_name) turning on tracing of test actions has been implemented
- Error diagnosis component has been integrated into the toolkit (experimental feature)
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
C++TESK Testing ToolKit v1.0.15 has been released. The following things have been done.
- User documentation has been updated
- Command line parameters --exit-at-cycle <cycle-number> and --exit-if-condition
have been added
- CoverageTracker's method isFullyCovered<CoverageType>() has been
implemented
- Further improvement of the Eclipse IDE plugin (still experimental) has been done
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
In frames of Google Summer of Code 2011 Ph.D. student Evgeny Novikov has successfully developed a project "User-friendly Interface for Linux Driver Verification Tools" with help of his mentor Alexey Khoroshilov for The Linux Foundation.
Within the given project a Knowledge Base support was developed. The Knowledge Base infrastructure allows users to keep results of unsafes analysis directly through the Statistics Server Web interface. Then these stored results are automatically applied to new uploaded unsafes in depend on different chosen comparison criteria. This significantly simplifies and speed ups the whole verification results analysis and makes the Linux Driver Verification project more attractive for end-users.
Also several minor issues of the Statistics Server related with usability and speed of page generation were resolved during Google Summer of Code 2011. One can see them here: #570, #1168, #1205, #1265, #1363, #1364, #1537, #1538
A Knowledge Base branch was merged to the master branch of the Linux Driver Verification project. It was successfully integrated with other tools, so stable Knowledge Base functionality is available beginning from 4ca264d.
We're going to continue develop and extend Knowledge Base infrastructure further. Keep in touch!
You may download sources and binaries on the Files page of the project. See also the original project page.
Release notes¶
Analysis speedup¶
- Fast and sound algorithm for alias analysis for pointers to structures without dereference depth limit enforced. Does not terminate on some programs with arbitrary-depth lists.
- Add some normalization for better caching of postcondition requests.
- Improved performance of lattice states merge.
New features¶
- Re-animated function pointer support (-fp), which, however, doesn't distpatch correctly two or more functions aliased by the pointer.
- Updated 64- and 32-bit versions of CSIsat allow you to analyze programs with as large numbers as your architecture supports.
Infrastructure improvements¶
- Separated supported and unsupported options. Most recently added options has been made default.
- Regression test suite may work in "competition" mode.
Bug fixes¶
- Formulae caching in O(logN) useful blocks algorithm fixed (less FOCIinterface.SAT exceptions).
C++TESK Testing ToolKit v1.0.14 has been released. A number of new features have been implemented.
- New version of VeriTool.
- Automatic catcher of unexpected reactions.
- Macro CPPTESK_SET_DEBUG_LOGFILE(filename) to duplicate debug output into a file.
- Basic Eclipse IDE plugin.
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
You may download sources and binaries on the Files page of the project. See also the original project page.
Release notes¶
Analysis speedup¶
- Speedup ranges from 8 times on small-sized programs to 30 times on medium-sized programs
- Logarithmic algorithm for useful-blocks (significantly speedup of trace analysis)
- Improved integration with SMT solvers
- efficient string concatenation
- caching of converted formulae
- optimization of CVC3 options for BLAST use cases
- Formulae normalization has been moved to solvers since solvers do it faster (option
-skipnorm)
- Alias analysis speedup
- must-aliases are handled separately and faster than may-aliases (option
-nomusts)
- removed unnecessary debug prints from alias iteration (even a check for debug flag impacts performance significantly in hot places)
- BLAST-specific tuning of OCaml virtual machine options (script
"ocamltune")
Important bug fixes¶
- Fixed unsound analysis when lattices are used (options
-stop-sep and -merge) (Time of analysis has been increased by a factor of 1.5, but the inherent imprecision in lattices no longer makes BLAST miss bugs). See bug #330
- bool-to-int casting in function calls fixed. See bug #334
Frontend¶
- C frontend (CIL) uplift, fixes and workarounds (see
-ignoredupfn and -nosserr options)
- Some errors have been made warnings
New features¶
- constrain stack depth to be analyzed; see options
-fdepth, -important-attrs, and -inline-attrs
- treat constant pointers as must aliases (see option
-const)
Infrastructure improvements¶
- Regression test suite improved
- Got rid of non-free software (Simplify solver was replaced by CVC3, ditched unused Vampyre, FOCI, and CLPprover)
C++TESK Testing ToolKit v1.0.13 has been released. The new features are as follows.
- Example illustrating usage of C++TESK in couple with SystemVerilog (counter_sv)
- Printing more information about MISSING, UNEXPECTED, and INCORRECT reactions
- Installation guide in English
- Support of 64-bit Linux systems
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
C++TESK web forums (one for Russian speakers and one for English speakers) opened today on http://forge.ispras.ru/projects/cpptesk-toolkit/boards.
We hope that forums will help both C++TESK users and developers. Users will be able to get useful information quickly and to exchange their experience, while developers will get immediate feedback from users.
Both forums are open for viewing; to post messages, an account is required. E-mail us to cpptesk-support [at] ispras.ru to get further information on how to get an account.
You are welcome to join the C++TESK community.
C++TESK Testing ToolKit v1.0.11 has been released. The following things have been done.
- Simple heuristic to avoid getting caught in an endless loop during non-deterministic graph traversal has been implemented
- Command line parameter --print-progress turning on the traversal progress printing has been added
- Example cache_coherence has been included to demonstrate methods for state abstraction and non-deterministic graph traversal
- One mistake in distributed test launching has been fixed
- Scripts have been improved
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.