Skip to content

Add coreutil benchmarks with generated assertions

Julian Erhard requested to merge erhardj/sv-benchmarks:main into main

This PR adds benchmarks that are based on GNU coreutil programs that were instrumented with assertions. For each coreutil program, there is a version with assertions generated from a constant-propagation (and exclusion set) analysis, and a second version, where additionally a interval analysis was performed.

When compiling the files with GCC, there are still some warnings present.

In particular, there are warnings about missing casts in the assertions, and for some apparently conflicting declarations of builtin functions. I plan to fix these.

The remaining warnings are of benign nature and it is documented in the Makefile why the specific warnings are deactivated.

TODO

  • Fix warnings about missing casts in asserts

  • Fix warnings about conflicting declarations of builtin functions

  • programs added to new and appropriately named directory

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

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

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

  • intended property matches the corresponding .prp file
  • programs and expected answer added to a .yml file according to task definitions
  • data model present in task-definition file
  • original (ideally not preprocessed) sources present
  • preprocessed files present
  • preprocessed files generated with correct architecture
  • Makefile added with correct content and without overly broad suppression of warnings
Edited by Julian Erhard

Merge request reports