Releases: sosy-lab/tbf
Minor bug fixes and test adjustments
We now only support python 3.5 and later.
Small bugs in python 3.5 and in tool execution
regarding unicode conversion were fixed that made
tbf crash if a tool printed unknown characters.
To make CI checks run more reliably, fix problems with test setup and too strict time limits.
v0.3.0-testcomp19: Test-Comp adjustments for v0.3.0 of tbf.
Fully C-based random tester.
PRTest, the random tester included with tbf,
is now fully C based and only writes meaningful tests
that cover new blocks.
This Test-Comp-specific release contains support for --spec
instead of --error-method
,
and lxml is included as additional library for execution on the Test-Comp clusters.
TBF, Version 0.2.1
Very minor change: TBF now actually says that it's version 0.2
when invoking tbf --version
.
TBF, Version 0.2
This release is a major cleanup of tbf and provides the possibility to do test-case generation and test-case execution in separate runs.
-
tbf is now executed through
bin/tbf
. -
If tbf is not told how to run test cases, it simply won't. So to create test cases, but not execute/validate them, omit both parameters
--execution
and--witness-validation
. -
To execute/validate existing test cases, use parameter
--use-existing-test-dir EXISTING_TESTS_DIR
with the directory that contains the test cases and the intended method (--execution
or--witness-validation
). You will still have to provide option--input-generator GENERATOR
to tell tbf
the format of the test cases, but it will not create any new test cases. -
Directory
contrib
contains benchmark definition files and a table definition file to use TBF with BenchExec for reproducible experiments.
For Developers:
The structure of tbf has changed.
Directory tbf
contains all program-related modules. Directory tbf/tools
contains all test-case generators and the corresponding python modules to run them from within tbf, and directory tbf/validators
contains the witness validators (currently CPAchecker and UAutomizer).
First official release
Contains support for AFL-fuzz, Crest, CPAtiger, FShell, Klee, and a simple random input generator that is part of this project.
It is possible to validate generated test cases using test case execution or potential witness validation with CPAchecker.
Witness validation using CPA-w2t, FShell-w2t and UAutomizer is experimental.