Project

General

Profile

News

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.9 released

Added by Alexander Kamkin over 13 years ago

C++TESK Testing ToolKit v1.0.9 has been released. The following features have been done.

  • The libmicrohttpd library has been included into the package
  • Bookmarks have been added to all of the documents
  • Debug printing has been improved (if an error happens inside a process, call stack is shown)
  • Macro CPPTESK_CALL_STACK() that can be used in CPPTESK_DEBUG_PRINT() has been added (it makes sense only in reference models)
  • Macros CPPTESK_SET_DEBUG_LEVEL() and CPPTESK_SET_DEBUG_STYLE() intended for debug printing setup have been implemented
  • Macros CPPTESK_COLORED_DEBUG_PRINT(F)() for colored debug printing have been added
  • Examples have been improved
  • A bug in the 64-bit message field randomization has been fixed
  • Macros CPPTESK_RANDOM_ENUM() and CPPTESK_RANDOM_CHOICE() have been implemented
  • Callback noEveryCycle() starting at each cycle of simulation has been added
  • Message fields validity check has been implemented (warning is printed if a field is uninitialized)
  • Quick reference has been updated (assertions, debug possibilities, etc.)

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.8 released

Added by Alexander Kamkin over 13 years ago

C++TESK Testing ToolKit v1.0.8 has been released. The following things have been done:

  • Bug in the process scheduling has been resolved (it occured while a newly created parallel process immediately finished)
  • Additional checking of the process calling stack has been inserted
  • Printing violated assertions to the utt2 trace has been implemented
  • Macroses for colored debug print have been added (CPPTESK_COLORED_DEBUG_PRINT(F))
  • Scripts "show current version" (version.sh) and "update me" (update.sh) have been added
  • Graphviz-based script "draw the image of the state graph" (graphviz.sh) has been added
  • Examples have been slightly updated

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.7 released

Added by Alexander Kamkin over 13 years ago

C++TESK Testing ToolKit v1.0.7 has been released. The following improvements have been done:

  • A memory leak problem has been found and solved
  • Caching mechanism for iteration context has been developed
  • Printing statistics on reactions at the end of testing has been added
  • Macros for registering incomparable message fields have been added
  • Slight improvement of the summary report generation
  • Highlighting of the installation progress

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.6 released

Added by Alexander Kamkin over 13 years ago

C++TESK Testing ToolKit v1.0.6 has been released. The following things have been done:

  • All the warnings appearing during the compilation with -Wextra flag have been removed
  • The documentation has been updated
  • Additional debug facilities have been added
  • Minor core improvement has been made
  • Examples have been slightly updated
  • Scripts for the SSH cluster have been added
  • New version of the VeriTool can be installed while using install.sh with --install-veritool flag

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

Linux Driver Verification: Version 0.3 of LDV Tools Released

Added by Pavel Shved over 13 years ago

The most significant changes include:
  • Three kernel rules were brought to a good quality level, and they now find more bugs: spin lock/unlock, memory allocation inside spin locks, and alloc/free urb — in addition to the good old mutex lock/unlock
  • New Aspectator (aspect-oriented programming tool for C) was integrated into the projects, and the structure and the variable names of a program processed now looks nearly as well as the original one
  • Concurrent and distributed execution of driver verification
  • Support of CPAchecker static analysis tool, as well as of BLAST

See the downloading instructions to get these tools.

The source code repository may be browsed by v0.3 tag.

KEDR: KEDR 0.3 released

Added by Eugene Shatokhin over 13 years ago

KEDR is an extensible system for dynamic analysis of kernel modules (device drivers, file system modules, etc.) in Linux. KEDR tools operate on the modules chosen by the user and can detect memory leaks, perform fault simulation and more.

This release provides several enhancements and various fixes compared to version 0.2.1. The most significant changes:

  • Handling of intercepted function calls has been revisited to allow doing several kinds of analysis at the same time (e.g. performing fault simulation and memory leak detection simultaneously).
  • The components responsible for fault simulation are now decoupled from call monitoring (call tracing) facilities and can be used independently if necessary.
  • Several enhancements and fixes have been applied to the trace capturing utility.
  • Stack trace-related API has been revisited and simplified. If the kernel provides reliable stack traces, the API works now even if save_stack_trace() is not available.
  • Handling of allocations and frees in the memory leak detector is now deferred via a work queue. This allows to significantly reduce the time spent with locks held.
(331-340/364)

Also available in: Atom