Skip to content
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.

Document requirements for benchmark submission #167

Closed
4 of 11 tasks
PhilippWendler opened this issue Oct 25, 2016 · 5 comments
Closed
4 of 11 tasks

Document requirements for benchmark submission #167

PhilippWendler opened this issue Oct 25, 2016 · 5 comments

Comments

@PhilippWendler
Copy link
Member

PhilippWendler commented Oct 25, 2016 •
edited

The following list of things is my check list for assessing pull request with new benchmarks.
Each of these items should probably be mentioned in the documentation.

  • license present and acceptable (cf. Define and check license requirements #165)
  • readme present
  • architecture (32 bit vs. 64 bit) stated
  • original sources present
  • preprocessed files present
  • preprocessed files generated with correct architecture
  • property file present (as long as property files are in subdirectories)
  • expected verdict in file names
  • build system adjusted for enabling checks of this directory
  • build system can build the new benchmarks without warnings (both with gcc and clang)
  • category file adjusted (cf. Should pull requests add new benchmarks to categories? #164)
dbeyer added a commit that referenced this issue Oct 29, 2016
@dbeyer
Checklist added, inspired by and copy&paste from #167
08354b9
@dbeyer
Copy link
Member

dbeyer commented Oct 29, 2016

Great idea! Thanks.
Done: checklist

@dbeyer
Copy link
Member

dbeyer commented Oct 29, 2016

Question: What is the trick for the markdown to show click boxes?

@kfriedberger
Copy link
Member

kfriedberger commented Oct 29, 2016 •
edited

  • either "add task list" from the buttons above the editor.
  • or type "- [ ] text"

@tautschnig
Copy link
Contributor

@PhilippWendler Shouldn't this issue be closed with 08354b9?

@PhilippWendler
Copy link
Member Author

I think it would be good to add an explanation to the documentation for each of the points, such that submitters can actually fulfill the requirements. Now it is more a checklist only for people that already know what each point means.

PhilippWendler added a commit that referenced this issue Sep 1, 2017
@PhilippWendler
Update documentation on how to submit verification tasks.
8886970 
- Move checklist for PRs to a PR template
  that GitHub will insert automatically in the description field for new PRs.
- Document everything that submitters should read in new file CONTRIBUTING.md,
  for which GitHub will automatically show a link when creating a new issue or PR.
- Remove content that is now in CONTRIBUTING.md from README.md.

Fixes #167.
@PhilippWendler PhilippWendler mentioned this issue Sep 1, 2017
Merged
PavelAndrianov added a commit to PavelAndrianov/sv-benchmarks that referenced this issue Nov 15, 2017
@PavelAndrianov
New subcategory systems:concurrency
fe8f2d1 
Based on Linux drivers

Fix sanity checks

Remove copy-pasted flag

The suppress_warnings flag is not neccesary

Disable particular warnings of CLANG

Minor change: remove comments

Fix problems with uninitizized variables

Minor changes

Add instructions for obtaining the benchmarks

Extract pthread-specific code into header file

Add stubs for all undefined functions

Update documentation on how to submit verification tasks.

- Move checklist for PRs to a PR template
  that GitHub will insert automatically in the description field for new PRs.
- Document everything that submitters should read in new file CONTRIBUTING.md,
  for which GitHub will automatically show a link when creating a new issue or PR.
- Remove content that is now in CONTRIBUTING.md from README.md.

Fixes sosy-lab#167.

use full links in PR template because otherwise links are broken

Adding a template for verification tasks, and a new template-set file

Add sanity checks for duplicate and contradicting properties

Fix bug in check.py that did not check for unknown violated properties

Adapt our varios check scripts to the new directories and files

Restructure and adjust headings

Add links to defining secions

The text should not be SV-COMP specific.

More on parameters

Describe the templates for verification tasks

Description and motivation of the repository

Added property 'memcleanup'

Benchmarks for testing operations on sets

Make list implementation of sets

Fix other examples

Add Makefile

Add preprocessed files

Add sets to ReachSafety-Heap

Add license

Add Readme

use 'cpp -P' for preprocessing

Move aux files to model dir

Replace license file by symlink

Ignore model dir

Enable warnings

Add empty Makefile (the model dir is ignored)

Suppress 'unexpected subdirectory model' for ldv-sets

Disable warnings about incompatible redeclaration of library functions

Not required

use -m32 for preprocessing

Add contributed by

Add test for unbounded case

Remove cillified files from repository for which we have corresponding non-cillified files.

These were removed from the actual benchmark sets 4 years ago in 4f80d53.

Remove duplicate files.

This fixes most of sosy-lab#445 according to the explanation from
sosy-lab#445 (comment)

Remove another duplicate file and ajust some filenames

as suggested by
sosy-lab#445 (comment)

Remove one of each of the remaining duplicate file pairs (picked arbitrarily)

Fix undefined behavior in volatile_alias.c

There was an assignment of the address of a volatile int to an int*
pointer, loosing the volatile modifier.
To keep the original intention of the benchmark,
there is now an assignment of the address of an int to a volatile int*.

Rename property to positive name

Rename categories with property NoOverflow to positive name

Fix link in README for renamed property

heap-manipulation: resolve function pointer with unspecified arguments (sosy-lab#462)

(*insert_fnc)() declares insert_fnc as a function pointer with an
unknown number and type of parameters, not with an empty list of
parameters.  This may be an underspecification that can lead to possible
undefined behaviour.  This commit fixes that in two benchmarks of
Predator.

heap_manipulation: commit also *.i files

heap-manipulation: fix problems with fnc pointers

heap-manipulation: fix *.i files

heap-manipulation: re-pre-process with -m32

Add model directory

Exclude model directory from building process
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@tautschnig @PhilippWendler @dbeyer @kfriedberger