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 #167.

.github/PULL_REQUEST_TEMPLATE

@@ -0,0 +1,22 @@
+<!--
+  Please describe your PR as usual.
+
+  For submission of new verification tasks,
+  keep the following checklist and make sure that all items are fullfilled.
+  For other PRs, just remove it.
+-->
+
+- [ ] programs added to new and [appropriately named](CONTRIBUTING.md#directory-structure-and-names) directory
+- [ ] license present and [acceptable](CONTRIBUTING.md#license) (either in separate file or as comment at beginning of program)
+- [ ] [contributed-by](CONTRIBUTING.md#origin-description-and-attribution) 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)
+- [ ] intended property matches the corresponding `.prp` file
+- [ ] expected answer in file names according to [convention](CONTRIBUTING.md#properties)
+
+<!-- For C programs: -->
+- [ ] [architecture](CONTRIBUTING.md#architecture) (32 bit vs. 64 bit) matches the corresponding `.cfg` file
+- [ ] original sources present
+- [ ] [preprocessed](CONTRIBUTING.md#preprocessing) files present
+- [ ] preprocessed files generated with correct architecture
+- [ ] [Makefile](CONTRIBUTING.md#compile-checks) added with correct content and without overly broad suppression of warnings

CONTRIBUTING.md

@@ -0,0 +1,154 @@
+# Contribution Guidelines
+
+If you have identified an issue with existing verification tasks,
+or want to submit new verification tasks,
+please [file an issue](https://github.com/sosy-lab/sv-benchmarks/issues/new)
+or, even better, submit a pull request.
+
+For issues with existing verification tasks that affect the expected answer of the task,
+it is helpful if you can additionally provide a machine-readable [witness](https://github.com/sosy-lab/sv-witnesses)
+that supports your claim.
+If such a case occurs, in general we try to fix the problem in the task
+while keeping the task's original intention,
+and at the same time add a copy of the unchanged problematic task
+with an appropriately updated expected answer.
+
+For new verification tasks, please read the remainder of this document.
+
+
+## How to Submit Verification Tasks to this Repository
+
+In order to contribute verification tasks, please use the following steps:
+- fork the repository,
+- commit your additions or changes to this repository,
+- file a pull request, and
+- discuss with community members until your contribution is approved and merged into the repository.
+
+
+### Directory Structure and Names
+
+In general, groups of new verification tasks should be added to a new directory
+under the respective language-specific directory.
+The name of this directory should describe the source and/or purpose of these verification tasks.
+
+The names of the individual files should be based on the file name or short title of the original program
+(for real-world source) or a description of what is verified in this verification task.
+
+Note that the file names of verification tasks need to be globally unique in the repository.
+
+
+### License
+
+The verification tasks need to be accompanied by a license,
+either via a file `LICENSE.txt` or similar in the same directory,
+or via a comment in the program header.
+If a common license is used, please use a symlink to an existing license file
+instead of adding an additional copy.
+
+The stated license must allow to:
+- view, understand, investigate, and reverse engineer the algorithm or system,
+- change the program (in particular, preprocess and adopt the programs to be useful for a verification task),
+- (re-)distribute the (original and changed) program under the same terms (in particular, in replication packages for research projects or as regression tests),
+- compile and execute the program (in particular, for the purpose of verifying that a specification violation exists), and
+- commercially take advantage of the program (in particular, to not exclude developers of commercial verifiers).
+
+If possible, standard open-source licenses such as Apache 2.0 or GPL are preferred.
+If you are submitting verification tasks that are based on third-party source code,
+make sure to follow the restrictions of the original license!
+For example, verification tasks based on GPL source code must be licensed under the GPL as well.
+
+
+### Origin, Description, and Attribution
+
+The subdirectories that contain the programs should contain a file `README.txt` or similar
+that gives further information about the programs.
+In particular, this is the place to describe the origin and to add any attribution.
+Please add a link to project web sites and any relevant publications in such a description.
+
+
+### C Programs
+
+For verification tasks written in C, some additional requirements are necessary.
+In general, we prefer source code that adheres to the ANSI C standard,
+but for real-world programs GNU C is also acceptable.
+
+#### Properties
+
+For each program, at least one [property](README.md#specification-properties)
+needs to be specified.
+
+For each property against which a program is to be verified,
+the string `_false-<property>` or `_true-<property>` needs to be included in the file name,
+according to the expected verification answer.
+For example, the program `minepump_spec5_product61_true-unreach-call_false-termination.cil.c`
+is expected to satisfy property `unreach-call` and to violate property `termination`.
+
+#### Category
+
+In order to be effectively used by people (e.g., in SV-COMP),
+the verification tasks need to be part of some category.
+Thus, please choose an appropriate category of [SV-COMP](https://sv-comp.sosy-lab.org/2017/benchmarks.php)
+and make sure that your programs are
+- matched by the `.set` file of the category by adding appropriate patterns,
+- are made to be verified against the specification in the `.prp` file of the category, and
+- are compatible to the parameters in the `.cfg` file of the category.
+
+Programs can also be part of several categories if more than one property is present.
+If a task does not fit in any existing category, you may propose a new category.
+
+#### Architecture
+
+Each category specifies an architecture (32-bit or 64-bit Linux systems) in its `.cfg` file,
+and all verification tasks of a category need to be valid
+assuming a system with the respective architecture.
+This mostly affects sizes of data types.
+Please check that the architecture of the category matches the one of your programs.
+
+#### Preprocessing
+
+For C programs with preprocessor directives (e.g., `#define`, `#ifdef`, or `#include`),
+in addition to the original `.c` (and `.h`) files,
+preprocessed files (extension `.i`) also need to be added.
+The reason for this is that preprocessing can produce different results
+depending on the version of installed libraries,
+and thus the precise nature of the verification tasks would depend on a user's system
+if non-preprocessed files would be used.
+Thus, only preprocessed files will be part of official verification tasks
+and may appear in `.set` files.
+
+For preprocessing, please make sure to follow these rules:
+- No `#line` directives should appear in the result (use `-P` flag for `cpp`).
+- Preferably use a recent `gcc` (e.g., on an Ubuntu 16.04 system).
+- The preprocessor needs to use the correct architecture
+  (pass `-m32` or `-m64` to `cpp` depending on whether you are submitting 32-bit or 64-bit programs).
+
+Of course, if the source code does not need preprocessing,
+this step is not necessary and the `.c` files can be used directly.
+
+#### Compile Checks
+
+Verification tasks in this repository need to be compilable, preferably without warnings.
+We use a continuous-integration to check this.
+In order to enable these checks for programs in a new directory,
+please add a `Makefile` in the directory with the following content:
+```
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config
+```
+If the programs are for 64-bit systems,
+additionally add `CC.Arch := 64` before the `include` line.
+
+Then run `make clean && make CC=gcc && make clean && make CC=clang` from a shell in your new directory.
+
+If some compiler warnings can not or should not be fixed, it is possible to whitelist them in the `Makefile`.
+Its is also possible to ignore specific files or directories that should not be checked.
+Please refer to the [Makefile documentation](c/Makefile-README.md) for more details.
+
+#### Sanity Checks
+
+We also have a script that performs some sanity checks on verification tasks.
+Please run [check.py](c/check.py) and check for any `ERROR`s reported.
+If some violation is on purpose (e.g., additional files that are no verification tasks),
+please whitelist the respective warning by adding it to one of the `KNOWN_*_PROBLEMS` lists
+in the script.

README.md

@@ -9,45 +9,67 @@
 This collection of verification tasks is constructed and maintained as a common benchmark
 for evaluating the effectiveness and efficiency of state-of-the-art verification technology.
 
+This repository is actively used by the competition on software verification [SV-COMP],
+which is the reason why some of the text below is specific to SV-COMP.
+
 The verification tasks were contributed by several research and development groups. 
-After the submission deadline of verification tasks for [SV-COMP](http://sv-comp.sosy-lab.org/),
+After the submission deadline of verification tasks for [SV-COMP],
 a group of people (organizer and participants) are working on improving the quality of the verification tasks.
 This means that after the sets were made public, some programs were removed
 (not qualified, no property encoded, unknown architecture), and 
-some programs got technically improved (CIL simplifications, compiler warnings, memory model).
+some programs got technically improved (compiler warnings, memory model).
 These changes have improved the overall quality of the final set of programs for the competition, and
 have not changed the intended verification result; all changes are tracked in the public repository.
 
+**This repository is open for submission of new verification tasks!**
+Please refer to our [contribution guidelines](CONTRIBUTING.md)
+to see how to submit verification tasks to this repository.
+
 Thanks to all contributors of programs, patches, and discussion comments.
 
 ### Structure
 
 The collection consists of three directories, which contain verification tasks written in different languages:
-- c/ (programming language C, follows the GNU C standard, many programs even adhere to ANSI C)
-- java/ (programming language Java)
-- causes/ (systems from the other directories translated to Horn clauses and stored in SMT format)
-
-This repository is actively used by the competition on software verification [SV-COMP](http://sv-comp.sosy-lab.org/),
-which is the reason why some of the text below is specific to SV-COMP.
+- `c/` (programming language C, follows the GNU C standard, many programs even adhere to ANSI C)
+- `java/` (programming language Java)
+- `causes/` (systems from the other directories translated to Horn clauses and stored in SMT format)
 
 ### License
 
-The programs are accompanied by a license, either via a file LICENSE.txt in the same directory,
+The programs are under different licenses, which are specified either via a file `LICENSE*.txt` in the same directory,
 or via a comment in the program header.
-The licenses must allow to:
-- view, understand, investigate, reverse engineer the algorithm or system,
-- change the program (in particular, pre-process and adopt the programs to be useful for a verification task),
-- distribute the (original and changed) program (in particular, in replication packages for research projects or as regression tests),
-- compile and execute the program (in particular, for the purpose of verifying that a specification violation exists), and
-- commercially take advantage of the program.
+Most of the programs are under an open-source license such as Apache 2.0 or GPL.
 
 ### Origin, Description, and Attribution
 
-The subdirectories that contain the programs contain files README.txt, which give further information
+The subdirectories that contain the programs contain files `README.txt`, which give further information
 about the programs, in particular, this is the place to trace the origin and to attribute the programs to their contributors.
-It is a good idea to link to project web sites and publications in those descriptions.
 For some programs, this information is given in the header of the program as comment.
 
+### Name Convention for Programs
+
+The program files in this repository are named as follows:
+- the original file name or short title of the program is given at the beginning,
+- for each property against which the program is to be verified,
+  the string `_false-<property>` or `_true-<property>` is included, according to the expected verification answer, and
+- the filename ends with ending `.c` for not preprocessed files and `.i` for preprocessed files (for C files).
+
+For example, the program `minepump_spec5_product61_true-unreach-call_false-termination.cil.c`
+is expected to satisfy property `unreach-call` and to violate property `termination`.
+
+There are some old programs that have ending `.c` although they are preprocessed.
+
+### Categories
+
+The verification tasks for C programs are grouped into (sub-)categories
+as defined by [SV-COMP](https://sv-comp.sosy-lab.org/2017/benchmarks.php).
+
+A (sub-)category `<category>` is defined by the following three files:
+- `<category>.set` contains patterns that specify the set of programs,
+- `<category>.prp` contains the specification, and
+- `<category>.cfg` contains the parameters (and a description of the (sub-)category).
+
+
 ## Definitions
 
 The following definitions are taken from the SV-COMP report
@@ -61,11 +83,8 @@ A *verification task* consists of
 A *category* is a set of verification tasks.
 
 A *sub-category* is a set of verification tasks that consist of the same
-specification and the same parameters.
-A sub-category <sub-category> is defined by the following three files:
-- <sub-category>.set contains patterns that specify the set of programs,
-- <sub-category>.prp contains the specification, and
-- <sub-category>.cfg contains the parameters (and a description of the sub-category).
+specification and the same parameters
+as specified in the corresponding `.cfg` and `.prp` files.
 
 A *verification run* is
 - a non-interactive execution
@@ -77,75 +96,22 @@ in order to check whether the following statement is correct:
 
 A *verification result* is a triple (ANSWER, WITNESS, TIME) with
 - ANSWER is an element from {TRUE, FALSE, UNKNOWN},
-- WITNESS is a violation witness or correctness witness that supports validation of the (untrusted) answer, and
+- WITNESS is a violation witness or correctness witness in the common [witness format] that supports validation of the (untrusted) answer, and
 - TIME is the CPU time that the verification run has consumed (in practice, also other resource measurement values are reported).
 
-## Name Convention for Programs
-
-A program file should be named as follows:
-- the original file name or short title of the program is given at the beginning,
-- for each property against which the program is to be verified,
-  the string `_false-<property>` or `_true-<property>` is included, according to the expected verification answer, and
-- the filename ends with ending .c for not pre-processed files and .i for pre-processed files.
-
-For example, the program `minepump_spec5_product61_true-unreach-call_false-termination.cil.c`
-is expected to satisfy property `unreach-call` and to violate property `termination`.
-
-There are some old programs that have ending .c although they are pre-processed.
-
-## How to Submit Verification Tasks to this Repository
-
-This collection relies on contributions from many people.
-In order to contribute verification tasks, please use the following steps:
-- fork the repository,
-- commit your additions or changes to this repository,
-- file a pull request, and
-- discuss with community members until your contribution is approved and merged into the repository.
-
-When pre-processing C files, please use the command `cpp -P` or something similar
-that does not add line directives to the output.
-Please make sure that you are pre-processing the files with the correct architecture
-(e.g., on a 64-bit system, you need to specify `-m32` for 32-bit programs)!
-
-#### Category
-
-In order to be effectively used by people (e.g., in SV-COMP), the verification tasks need to be part of some category.
-Thus, please make sure that your programs are 
-- matched by the .set file,
-- are made to be verified against the specification in the .prp file, and
-- are compatible to the parameters in the .cfg file
-of the category.
-
-#### Checklist for Assessing New Verification Tasks
-
-For approving a pull request, it is a good idea to copy&paste the following
-checklist as comment to the pull request:
-
-- [ ] license present and acceptable (either in LICENCE.txt or as comment at beginning of program)
-- [ ] contributed-by present (either in README.txt or as comment at beginning of program
-- [ ] programs added to a .set file of an existing category, or new sub-category established (if justified)
-
-- [ ] intended property matches the corresponding .prp file
-- [ ] architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
-- [ ] original sources present
-- [ ] preprocessed files present
-- [ ] preprocessed files generated with correct architecture
-
-- [ ] expected answer in file names according to convention
-- [ ] build system adjusted for enabling checks of this directory
-- [ ] build system can build the new benchmarks without warnings (both with gcc and clang)
 
 ## Specification Properties
 
-For SV-COMP, the [rules page](http://sv-comp.sosy-lab.org/2017/rules.php) explains all currently supported properties:
-  - [unreach-call](https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/PropertyUnreachCall.prp):
+For SV-COMP, the [rules page](https://sv-comp.sosy-lab.org/2017/rules.php) explains all currently supported properties:
+  - [unreach-call](c/PropertyUnreachCall.prp):
     A certain function call must not be reachable in the program.
-  - [valid-memsafety, valid-deref, valid-free, valid-memtrack](https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/PropertyMemSafety.prp):
+  - [valid-memsafety, valid-deref, valid-free, valid-memtrack](c/PropertyMemSafety.prp):
     A certain memory safety property must hold in the program.
     "memsafety" is the conjunction the other three properties.
-  - [no-overflow](https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/PropertyOverflow.prp):
+  - [no-overflow](c/PropertyOverflow.prp):
     A certain kind of undefined behavior (overflows of signed ints) must not be present in the program.
-  - [termination](https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/PropertyTermination.prp):
+  - [termination](c/PropertyTermination.prp):
     The program must terminate on all execution paths.
 
-
+[SV-COMP]: https://sv-comp.sosy-lab.org/
+[witness format]: https://github.com/sosy-lab/sv-witnesses