Merge pull request #1203 from sosy-lab/license-pthread

Add license declarations to all files in c/pthread

Author: dbeyer

.reuse/dep5

@@ -22,7 +22,6 @@ Files:
  c/loops
  c/ntdrivers
  c/ntdrivers-simplified
- c/pthread
  c/pthread-ext
  c/seq-pthread
  c/systemc

c/pthread/README.md

@@ -0,0 +1,17 @@
+<!--
+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
+-->
+
+Various small concurrent programs.
+
+- `bigshot*`, `sigma*`, `singleton*`: Submitted by the CSeq project
+- `triangular*`: Submitted by the CPAchecker project
+- Remainder submitted by the ESBMC project.
+  Some of these are described in https://doi.org/10.1145/1985793.1985839
+  or https://dl.acm.org/doi/10.1145/1639622.1639631 (also cf. https://wiki.cs.byu.edu/vv-lab/concurrency-tool-comparison).
+

c/pthread/README.txt

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }

c/pthread/bigshot_p.c

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 
 extern void __assert_fail (const char *__assertion, const char *__file,

c/pthread/bigshot_p.i

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }

c/pthread/bigshot_s.c

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 
 extern void __assert_fail (const char *__assertion, const char *__file,

c/pthread/bigshot_s.i

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }

c/pthread/bigshot_s2.c

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The CSeq project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 
 extern void __assert_fail (const char *__assertion, const char *__file,

c/pthread/bigshot_s2.i

@@ -1,3 +1,11 @@
+// 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-FileCopyrightText: The ESBMC project
+//
+// SPDX-License-Identifier: Apache-2.0
+
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }