aufover-benchmark
=================
A unified set of automated tests for multiple formal verification tools
(cbmc, symbiotic, divine) as well as static analysis tools (gcc, clang,
cppcheck).


How to run existing tests?
--------------------------
- enable yum/dnf repositories from `aufover` COPRs:
    $ sudo dnf copr enable -y @aufover/csdiff
    $ sudo dnf copr enable -y @aufover/divine
    $ sudo dnf copr enable -y @aufover/predator
    $ sudo dnf copr enable -y @aufover/symbiotic

- install required/optional dependencies of the benchmark on the system:
    $ make install-deps

- configure the benchmark:
    $ make

- run the tests:
    $ make check

- look for Label Time Summary in the output, it will tell you:
    - which tools actually ran
    - how many tests each of them analyzed (you need to divide the numbers by 4)
    - how much time it took for each of the tools


Alternative ways of running tests
---------------------------------
- passing custom options to ctest:
    $ CTEST_OPTS='-LE divine' make check    # exclude Divine tests

- using a custom working directory:
    $ mkdir /tmp/my-custom-wd
    $ WORKDIR=/tmp/my-custom-wd make check [-C PATH_TO_THIS_REPO]

- using source directory as a working directory:
    $ cd tests
    $ cmake .
    $ ctest -j16 --progress         # see doc/cmake.txt for other useful options

- select tests by labels (expected to be run from a working directory):
    $ ctest --print-labels
    $ ctest -L cbmc
    $ ctest -LE EXPENSIVE

- running selected tests (expected to be run from a working directory):
    $ ctest --show-only
    $ ctest -R test-0006
    $ ctest -E predator-regre


Formal verification of RPM packages (expensive)
-----------------------------------------------
- run all tests:
    $ sudo dnf install cmake koji make csmock-plugin-{cbmc,divine,symbiotic}
    $ make check-csmock

- passing custom options to ctest:
    $ CTEST_OPTS='-L symbiotic' make check-csmock   # use only Symbiotic
    $ CTEST_OPTS='-R coreutils' make check-csmock   # verify only coreutils
    $ CTEST_OPTS='--verbose' make check-csmock      # provide verbose output

- passing custom options to cmake:
    $ make check-csmock MOCK_PROFILE=fedora-34-x86_64
    $ make check-csmock CSMOCK_ADD_OPTS=--use-ldpwrap


Tree layout of this repository
------------------------------
/Makefile               top-level Makefile (its use is optional)
/doc                    documentation
/tests                  source code of the benchmark
/tests/CMakeLists.txt   top-level CMake configuration file
/tests/rpm-pkgs         test-suite that uses csmock to formally verify RPM pkgs
/tests/rpm-pkgs/README  information specific to the rpm-pkgs test-suite
/tests/single-c         simplified test-suite using single C file for each test
/tests/single-c/README  information specific to the single-c test-suite
/tests/*/sync.sh        scripts for syncing of expected results (use with care)
/workdir                default working directory (its use is optional)
/workdir-for-sync       separate working directory for sync script(s)