Source: cbmc
Section: science
Priority: optional
Maintainer: Michael Tautschnig <mt@debian.org>
Build-Depends:
 debhelper-compat (= 13),
 bison,
 flex,
 minisat (>= 1:2.2.1-2),
 zlib1g-dev,
 gdb [amd64],
 libxml2-utils,
 python-is-python3,
 z3 [!sh4],
 cvc5 [!armel !armhf !i386 !mips64el !hppa !hurd-amd64 !hurd-i386 !ia64 !loong64 !powerpc !sh4 !x32],
 default-jdk-headless [!arc !hppa !hurd-i386 !kfreebsd-amd64 !kfreebsd-i386 !loong64],
 libmaven-dependency-plugin-java [!arc !hppa !hurd-i386 !kfreebsd-amd64 !kfreebsd-i386 !loong64],
 libmaven-install-plugin-java [!arc !hppa !hurd-i386 !kfreebsd-amd64 !kfreebsd-i386 !loong64],
 maven-debian-helper [!arc !hppa !hurd-i386 !kfreebsd-amd64 !kfreebsd-i386 !loong64]
Standards-Version: 4.7.0
Homepage: http://www.cprover.org/cbmc/
Rules-Requires-Root: no

Package: cbmc
Architecture: any
Depends: gcc, ${shlibs:Depends}, ${misc:Depends}
Suggests: gdb
Description: bounded model checker for C and C++ programs
 CBMC generates traces that demonstrate how an assertion can be violated, or
 proves that the assertion cannot be violated within a given number of loop
 iterations.

Package: jbmc
Architecture: alpha amd64 arm64 armel armhf i386 ia64 m68k mips64el mipsel powerpc ppc64 ppc64el riscv64 s390x sh4 sparc64 x32
Depends: ${shlibs:Depends}, ${misc:Depends}
Suggests: java-compiler
Description: bounded model checker for Java programs
 JBMC generates traces that demonstrate how an assertion can be violated, or
 proves that the assertion cannot be violated within a given number of loop
 iterations.