Draft: Semtransforms recursion from loops

Dear SV-COMP community,

We would like to contribute a new set of benchmark tasks for the recursion category. The tasks are automatically generated by transforming loops into tail-recursive functions. As a starting point for the benchmark, we used several benchmark tasks from the Loops category (esp. < categories >). We think that our benchmark tasks could be an interesting challenge for the community, as the verifiers not only have to keep track of the recursion but also of varaibles that are provided as pointers.

For more details on the benchmark generation process, please refer to our tool semtransforms.

• programs added to new and appropriately named directory

  • recursified_loop-crafted
  • recursified_loop-invariants
  • recursified_loop-simple
  • recursified_nla-digbench

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

  • A few authors are unknown

• 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)

  • ReachSafety-Recursive.set

• suggest to add it to benchmark definitions (.XML) in repositories for benchmark-definitions

  • probably not necessary as we do not introduce a new category

• intended property matches the corresponding .prp file

  • unchanged

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

  • unchanged

• data model present in task-definition file
  • unchanged
• original (ideally not preprocessed) sources present
  • directly working on preprocessed files, thus there are no unprocessed sources
• preprocessed files present
• preprocessed files generated with correct architecture
  • directly working on preprocessed files
• Makefile added with correct content and without overly broad suppression of warnings
  • programs can be parsed by gcc without additional arguments/ makefile