Merge pull request #1099 from sosy-lab/reuse

Initial preparation for making the repo REUSE-compliant

Author: dbeyer

.github/PULL_REQUEST_TEMPLATE

@@ -7,7 +7,7 @@
 -->
 
 - [ ] programs added to new and [appropriately named](https://github.com/sosy-lab/sv-benchmarks/blob/master/CONTRIBUTING.md#directory-structure-and-names) directory
-- [ ] license present and [acceptable](https://github.com/sosy-lab/sv-benchmarks/blob/master/CONTRIBUTING.md#license) (either in separate file or as comment at beginning of program)
+- [ ] license present and [acceptable](https://github.com/sosy-lab/sv-benchmarks/blob/master/CONTRIBUTING.md#license) (in machine-readable comment at beginning of program as specified by the [REUSE project](https://reuse.software/))
 - [ ] [contributed-by](https://github.com/sosy-lab/sv-benchmarks/blob/master/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)

.github/PULL_REQUEST_TEMPLATE.license

@@ -0,0 +1,6 @@
+This file is part of the SV-Benchmarks collection of verification tasks:
+https://github.com/sosy-lab/sv-benchmarks
+
+SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+
+SPDX-License-Identifier: Apache-2.0

.github/workflows/reuse.yml

@@ -0,0 +1,18 @@
+# This file is part of the SV-Benchmarks collection of verification tasks:
+# https://github.com/sosy-lab/sv-benchmarks
+#
+# SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community
+#
+# SPDX-License-Identifier: Apache-2.0
+
+name: REUSE Compliance Check
+
+on: [push, pull_request]
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v2
+    - name: REUSE Compliance Check
+      uses: fsfe/[email protected]

.gitignore

@@ -1,3 +1,10 @@
+# This file is part of the SV-Benchmarks collection of verification tasks:
+# https://github.com/sosy-lab/sv-benchmarks
+#
+# SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+#
+# SPDX-License-Identifier: Apache-2.0
+
 *.class
 *.jar
 *.zip

.gitlab-ci.yml

@@ -1,3 +1,10 @@
+# This file is part of the SV-Benchmarks collection of verification tasks:
+# https://github.com/sosy-lab/sv-benchmarks
+#
+# SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+#
+# SPDX-License-Identifier: Apache-2.0
+
 stages:
   - images
   - checks
@@ -164,3 +171,12 @@ build-docker:java:latest:
     DOCKERFILE: java/.Dockerfile
     IMAGE: ci/java:latest
 
+
+# check license declarations etc.
+reuse:
+  stage: checks
+  image:
+    name: fsfe/reuse:latest
+    entrypoint: [""]
+  script:
+    - reuse lint

.reuse/dep5

@@ -0,0 +1,158 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: SV-Benchmarks
+Source: https://github.com/sosy-lab/sv-benchmarks
+
+Files:
+ c/*.set
+ c/*/*.yml
+ java/*.set
+ java/*/*.yml
+Copyright: 2011-2020 The SV-Benchmarks Community
+License: CC0-1.0
+
+Files:
+ clauses
+ c/bitvector
+ c/ddv-machzwd
+ c/ldv-memsafety
+ c/ldv-regression
+ c/ldv-README.txt
+ c/list-properties
+ c/locks
+ c/loops
+ c/ntdrivers
+ c/ntdrivers-simplified
+ c/pthread
+ c/pthread-ext
+ c/seq-pthread
+ c/systemc
+ java/rtems-lock-model
+ _
+Copyright: unknown
+License: LicenseRef-unknown
+
+Files:
+ c/Juliet_Test
+ c/array-cav19
+ c/array-crafted
+ c/array-examples
+ c/array-fpi
+ c/array-industry-pattern
+ c/array-lopstr16
+ c/array-memsafety
+ c/array-memsafety-realloc
+ c/array-multidimensional
+ c/array-patterns
+ c/array-programs
+ c/array-tiling
+ c/aws-c-common
+ c/bitvector-loops
+ c/bitvector-regression
+ c/busybox-1.22.0
+ c/eca-programs
+ c/eca-rers2012
+ c/eca-rers2018
+ c/float-benchs
+ c/float-newlib
+ c/floats-cbmc-regression
+ c/floats-cdfpl
+ c/floats-esbmc-regression
+ c/forester-heap
+ c/goblint-regression
+ c/heap-data
+ c/heap-manipulation
+ c/ldv-challenges
+ c/ldv-commit-tester
+ c/ldv-consumption
+ c/ldv-linux-3.0
+ c/ldv-linux-3.12-rc1
+ c/ldv-linux-3.14
+ c/ldv-linux-3.14-races
+ c/ldv-linux-3.16-rc1
+ c/ldv-linux-3.4-simple
+ c/ldv-linux-3.7.3
+ c/ldv-linux-4.0-rc1-mav
+ c/ldv-linux-4.2-rc1
+ c/ldv-memsafety-bitfields
+ c/ldv-multiproperty
+ c/ldv-races
+ c/ldv-sets
+ c/ldv-validator-v0.6
+ c/ldv-validator-v0.8
+ c/list-ext-properties
+ c/list-ext2-properties
+ c/list-ext3-properties
+ c/list-simple
+ c/loop-acceleration
+ c/loop-crafted
+ c/loop-floats-scientific-comp
+ c/loop-industry-pattern
+ c/loop-invariants
+ c/loop-invgen
+ c/loop-lit
+ c/loop-new
+ c/loop-simple
+ c/loops-crafted-1
+ c/memory-alloca
+ c/memsafety
+ c/memsafety-bftpd
+ c/memsafety-ext2
+ c/memsafety-ext3
+ c/nla-digbench
+ c/nla-digbench-scaling
+ c/openbsd-6.2
+ c/openssl
+ c/openssl
+ c/openssl
+ c/openssl
+ c/openssl-simplified
+ c/openssl-simplified
+ c/openssl-simplified
+ c/openssl-simplified
+ c/product-lines
+ c/psyco
+ c/pthread-C-DAC
+ c/pthread-atomic
+ c/pthread-complex
+ c/pthread-divine
+ c/pthread-driver-races
+ c/pthread-lit
+ c/pthread-memsafety
+ c/pthread-nondet
+ c/pthread-wmm
+ c/recursive
+ c/recursive-simple
+ c/recursive-with-pointer
+ c/reducercommutativity
+ c/regression
+ c/seq-mthreaded
+ c/seq-mthreaded-reduced
+ c/signedintegeroverflow-regression
+ c/sqlite
+ c/termination-15
+ c/termination-crafted
+ c/termination-crafted-lit
+ c/termination-dietlibc
+ c/termination-memory-alloca
+ c/termination-memory-alloca-todo
+ c/termination-memory-linkedlists
+ c/termination-numeric
+ c/termination-recursive-malloc
+ c/termination-restricted-15
+ c/termination-restricted-15-todo
+ c/verifythis
+ c/xcsp
+ java/MinePump
+ java/algorithms
+ java/java-ranger-regression
+ java/java-ranger-regression
+ java/jayhorn-recursive
+ java/jbmc-regression
+ java/jdart-regression
+ java/jdart-regression
+ java/jdart-regression
+ java/jpf-regression
+ java/juliet-java
+ _
+Copyright: unknown
+License: LicenseRef-in-text-file

.reuse/templates/header.jinja2

@@ -0,0 +1,10 @@
+This file is part of the SV-Benchmarks collection of verification tasks:
+https://github.com/sosy-lab/sv-benchmarks
+
+{% for copyright_line in copyright_lines %}
+{{ copyright_line }}
+{% endfor %}
+
+{% for expression in spdx_expressions %}
+SPDX-License-Identifier: {{ expression }}
+{% endfor %}

.travis.yml

@@ -1,3 +1,10 @@
+# This file is part of the SV-Benchmarks collection of verification tasks:
+# https://github.com/sosy-lab/sv-benchmarks
+#
+# SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+#
+# SPDX-License-Identifier: Apache-2.0
+
 # trigger build for only pull requests.
 if: type = pull_request
 

CONTRIBUTING.md

@@ -1,3 +1,12 @@
+<!--
+This file is part of the SV-Benchmarks collection of verification tasks:
+https://github.com/sosy-lab/sv-benchmarks
+
+SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
 # Contribution Guidelines
 
 If you have identified an issue with existing verification tasks,
@@ -39,11 +48,25 @@ Note that the file names of verification tasks need to be globally unique in the
 
 ### 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.
+All files need to have a copyright statement and a license declaration
+in a machine-readable comment at the beginning.
+We follow the current version of the [REUSE Specification](https://reuse.software/spec/),
+for more information and tool support cf. the [tutorial](https://reuse.software/tutorial/)
+and [FAQ](https://reuse.software/faq/) of the REUSE project.
+
+Example:
+```
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2020 ...
+//
+// SPDX-License-Identifier: Apache-2.0
+```
+Such a header can be easily created with the [reuse tool](https://github.com/fsfe/reuse-tool/):
+```
+reuse addheader --template header.jinja2 --copyright "..." --license Apache-2.0 yourfile.c
+```
 
 The stated license must allow to:
 - view, understand, investigate, and reverse engineer the algorithm or system,
@@ -52,10 +75,18 @@ The stated license must allow to:
 - 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 possible, standard open-source licenses such as Apache 2.0 or GPL are preferred,
+but custom licenses are possible
+(in the header, these need to be indicated as `LicenseRef-$NAME`
+and a file named `LicenseRef-$NAME.txt` with the license needs to be created
+in the `LICENSES` directory.
+
 If you are submitting verification tasks that are based on third-party source code,
-make sure to follow the restrictions of the original license!
+**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.
+Furthermore, the most common open-source licenses all require
+that any existing copyright notices are kept intact,
+do not delete them and make sure that any preprocessing also preserves them.
 
 
 ### Origin, Description, and Attribution