New tasks: Manually written tasks from coreutils v9.5
This MR proposes new verification tasks created from coreutils v9.5 through manually written verification harnesses.
The tasks use as much unmodified code from coreutils as possible. We only override (a) functions that are irrelevant to verification and produce a lot of bloat (see below), and (b) functions that use inline assembly.
The verification tasks are picked manually, to cover functional units of code included in coreutils. At the time of writing, we include verification tasks in three variants:
- Functionality tasks check postconditions on the code under verification.
- Cover-target tasks include a call to reach-error after the code under verification was called. This checks whether verifiers can pass through the code successfully.
- Cover-proof tasks include a call to reach-error after the post-condition checks. This checks whether verifiers can pass through the code and the post-condition checks successfully.
-
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) (Proposal: Added to SoftwareSystems-coreutils) -
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