^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
   ———      |     |   |   |     |   |   ||    |  |         |    |
  —(o)—     |     |   |   |     |   |   |  |  |  |————     '————|
 ———————    |     |   |    |   |    |   |    ||  |              |
—————————   —————'   —'—     '     —'—  '     '  '—————         '

This page corresponds to the submission of DIVINE-SMT to SV-COMP 2019.

Installation

DIVINE should work on any reasonably recent Linux distribution. It might also be possible to make it work on macOS, *BSD or even on Windows using Windows Subsystem for Linux, but this is not tested routinely.

Binary Distribution

The binary distribution is intended for SV-COMP and therefore should work on Ubuntu 18.04. However, as a binary distribution, it might not work on other Linux distributions or even on Ubuntu due to updates.

To use it, it is sufficient to extract the archive. Then run ./divine help in the main archive directory. If this succeeds (gives you a list of commands), you should be good to go with the binary distribution, if not, you should build DIVINE from the sources as your system is not compatible with the SV-COMP archive.

Building from Source

To build from the source, you will need some prerequisites, namely a C++11 compiler such as reasonably recent GCC (>= 4.9) or Clang (>= 3.2), make, CMake (>= 3.2), libedit, perl, and about 12GB of disk space and 4GB or RAM. For the symbolic verification to work as in SV-COMP, you will also need the Z3 solver, including its libraries.

You should extract the archive and then run make divine in its main directory. This should build DIVINE into _build.release/tools subdirectory by default. For more details, please refer to the manual.

Usage

If you use the binary distribution, both the SV-COMP wrapper (divine-svc) and the main DIVINE binary divine, are located in the divine-svc directory of the archive. If you have built DIVINE from the source, the wrapper resides in tools/divine-svc, while the built binary resides in _build.release/tools/divine.

In order to analyze an SV-COMP benchmark, you will also need a checkout of the SV-Benchmarks repository. Then you can analyze a benchmark as follows:

PATH_TO_DIVINE_WRAP/divine-svc PATH_TO_DIVINE_BIN PROPERTY.prop BENCHMARK.i

Where PATH_TO_DIVINE_WRAP is the path where divine-svc resides, PATH_TO_DIVINE_BIN is the path where the binary resides. The last line of the result should be the result given in SV-COMP.

Description of the Wrapper

The divine-svc wrapper handles translation from the SV-COMP property specification to DIVINE’s options and configuration based on some main features of the program.

• It enables some additional static analysis, namely options --svcomp (which ensures atomic sections work and resolves simple cases of bounded nondeterminism), and --lart stubs and --lart fixglobals (which attempt to work-around undefined functions and variables).
• It sets which properties should be reported as errors (e.g. leak checking is disabled for categories other then MemSafety, non-zero exit code is always ignored, …).
• It checks if the program contains any pthread_* functions and if not it enables --sequential to run DIVINE in sequential mode where it does not check for visibility of actions.
• It passes -fgnu89-inline to the compiler to make sure inline functions work as expected by SV-COMP (as DIVINE does not support C89, only C99).
• If any __VERIFIER_nondet_* function is found in the program, adds --symbolic option to enable SMT-based symbolic verification
• It wraps arguments of __VERIFIER_assert calls with double negation (!!(arg)) to work-around the fact that __VERIFIER_assert takes an int and therefore can truncate pointer values passed to it, especially in benchmarks intended to be verified as 32-bit (DIVINE does not support 32bit mode and often produces pointers with lower 32 bits equal to zero).