Dear mentors,

I am looking for a sponsor for my package "esbmc":

 * Package name     : esbmc
   Version          : 8.3.0+dfsg-4
   Upstream contact : ESBMC Development Team <esbmc@esbmc.org>
 * URL              : https://esbmc.org
 * License          : Apache-2.0 and BSD-4-Clause
 * Vcs              : https://github.com/esbmc/esbmc
   Section          : devel

The source builds the following binary packages:

  esbmc - Efficient SMT-based Context-Bounded Model Checker

ESBMC is a context-bounded model checker for the verification of single- and multi-threaded C/C++ and Python programs. It can automatically verify safety properties such as array bounds, pointer safety, and arithmetic overflow using SMT solvers including Z3.

To access further information about this package, please visit the
following URL:

https://mentors.debian.net/package/esbmc/

Alternatively, you can download the package with 'dget' using this command:

  dget -x https://mentors.debian.net/debian/pool/main/e/esbmc/esbmc_8.3.0+dfsg-4.dsc

ITP bug: https://bugs.debian.org/1138660

Changes since the last upload:

  * Fix debian/watch: switch to mode=git to bypass GitHub's
    JavaScript-rendered tags page; use dversionmangle to strip +dfsg
    and .0 suffix from the Debian version for comparison with
    upstream's 2-part tags (e.g. v8.3). uscan now correctly reports
    the package as up to date.

Lintian output for 8.3.0+dfsg-4 shows only experimental (X) tags;
no errors or warnings.

Regards,
Weiqi Wang

Hi Michael,

I have packaged ESBMC for Debian and I am looking for a sponsor. The RFS bug is #1139283, and the package is on mentors:

  dget -x https://mentors.debian.net/debian/pool/main/e/esbmc/esbmc_8.4+dfsg-1.dsc

https://mentors.debian.net/package/esbmc/
https://salsa.debian.org/WeiqiWang/esbmc

I am writing to you specifically because you maintain cbmc, boolector, minisat2 and picosat. ESBMC is a bounded model checker forked from CBMC some years ago, and it uses boolector as one of its solver backends, so it sits in the same corner of the archive as the packages you already carry. The Debian build currently enables Z3 only, to keep the initial package simple.

State of the package: it has been through two rounds of review on mentors and everything raised is addressed, it builds with sbuild against unstable, and Salsa CI is green. It is a single binary package.

Two things I should be upfront about. This would be my first package in Debian, so it needs to go through NEW. And I used an LLM to help with the packaging, then went back over all of it myself with the tools the manuals recommend; I take responsibility for the current version.

So the question: would you be able to sponsor the upload? If it is not something you have time for, could you point me at a DD who might be willing to look? Either answer is genuinely useful, and I am happy to make any changes you want first.

Thanks,
Weiqi Wang

The details in my original report are out of date, so here is the current state of this request.

The package on mentors is now 8.4+dfsg-1:

  dget -x https://mentors.debian.net/debian/pool/main/e/esbmc/esbmc_8.4+dfsg-1.dsc
https://mentors.debian.net/package/esbmc/

The 8.3.0+dfsg-4 URL in my original report no longer exists. The packaging git is on salsa, not the upstream github repository I gave originally:

https://salsa.debian.org/WeiqiWang/esbmc

Two people have reviewed the package on mentors rather than here, and everything they raised is addressed.

Bo YU (8 June): the changelog is now a single initial-release entry, Vcs-* point at salsa, Salsa CI is enabled, and the versioned LLVM and clang build-dependencies are replaced by the unversioned defaults.

Seyed Mohamad Amin Modaresi (late July): the upstream version now follows the v8.4 tag rather than upstream's CMakeLists.txt, d/watch is the version 5 file he supplied, d/source/options is gone, and d/copyright declares a single ESBMC licence for Files: * rather than listing Apache-2.0 and BSD-4-Clause side by side.

Built with sbuild against unstable, Salsa CI green.

One disclosure I made on the duplicate bug #1141762, which belongs here too: I used an LLM to help with the packaging. I went back over all of it myself with the tools the manuals recommend, and I take responsibility for the current version.

Two lintian tags show on mentors that do not appear with the lintian in unstable, both from the older lintian mentors runs: missing-debian-watch-file-standard, which does not recognise the deb822 "Version: 5" header in a version 5 watch file, and package-uses-experimental-debhelper-compat-version for debhelper-compat 14.

Still looking for a sponsor. Happy to fix anything that comes up.

Thanks,
Weiqi