Darksea's bitwise termination bechmarks used in aplas21 paper.

[cyruliu]

Dear SV-COMP Community,

We would like to contribute our bwb(Bitwise with Branching) termination benchmarks used in our work Proving LTL Properties of Bitvector Programs and Decompiled Binaries, which was accepted to APLAS'21, to sv-benchmarks. The benchmarks were added into the folder c/termination-bwb. Please let us know if there are any issues.

Thank you very much for your consideration. We are looking forward to your acceptance.

Best Regards, On behalf of our team, Y. Cyrus Liu

• [x] programs added to new and appropriately named directory

• [x] license present and acceptable (in machine-readable comment at beginning of program as specified by the REUSE project)

• [x] contributed-by present (either in README file or as comment at beginning of program)

• [ ] programs added to a .set file of an existing category, or new sub-category established (if justified)

• [x] intended property matches the corresponding .prp file

• [x] programs and expected answer added to a .yml file according to task definitions

• [x] data model present in task-definition file
• [x] original (ideally not preprocessed) sources present
• [x] preprocessed files present
• [x] preprocessed files generated with correct architecture
• [x] Makefile added with correct content and without overly broad suppression of warnings

[PhilippWendler]

Thanks!

Two first comments that might be helpful already while this is in draft status:

• As long as your .c files do not use #include, there is no need to preprocess them and add .i files. You can remove the latter.
• We have started using the format proposed by REUSE for adding license and copyright notices. Please use this for all files (and then you can remove your LICENSE.txt). The reuse addheader tool can automate adding the license headers.

[cyruliu]

Hi @PhilippWendler ,

Thank you so much for the comments! I updated the license to REUSE format, and remove the unnecessary preprocess files, can you help to review the benchmarks? Please let me know if there are other issues, thank you!

Best, Cyrus

[PhilippWendler]

Thanks!

I noticed that the SPDX information is different from authors and license in the readme.md, which of these is correct?

And is this the full collection from https://graphics.stanford.edu/~seander/bithacks.html or just a few select examples? Because the license info on that page is a little bit unclear when someone copies the whole collection?

[cyruliu]

Hi @PhilippWendler,

The SPDX information should be used, and just a few selected code snippet examples are from bithacks public domain, for clarity, I update the content of readme.md, please check, thank you!

Best, Cyrus

[PhilippWendler]

Looks good, I guess.

Now which category should these be added to? Termination-BitVectors.set?

[cyruliu]

Hi @PhilippWendler ,

That sounds good, I didn't see Termination-BitVectors.set in the repo, it would be great if the benchmarks I'm submitting can be added to it, thank you!

[PhilippWendler]

Yes, that would be a new subcategory. @dbeyer What do you think?