Add spdx licenses to seq-mthreaded

.reuse/dep5

@@ -125,7 +125,6 @@ Files:
  c/recursive-with-pointer
  c/reducercommutativity
  c/regression
- c/seq-mthreaded
  c/seq-mthreaded-reduced
  c/signedintegeroverflow-regression
  c/sqlite

c/seq-mthreaded/README.txt → c/seq-mthreaded/README.md

@@ -1,3 +1,13 @@
+<!--
+This file is part of the SV-Benchmarks collection of verification tasks:
+https://github.com/sosy-lab/sv-benchmarks
+
+SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+
+SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
+-->
+
 Contributed by: [HCCPS](http://www.sei.cmu.edu/cyber-physical/research/high-confidence) project
 
 The verification tasks should have the following convention:

c/seq-mthreaded/pals_STARTPALS_ActiveStandby.1.ufo.BOUNDED-10.pals.c

@@ -2,60 +2,13 @@ extern void abort(void);
 extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
 void reach_error() { __assert_fail("0", "pals_STARTPALS_ActiveStandby.1.ufo.BOUNDED-10.pals.c", 3, "reach_error"); }
 
-/**********************************************************************
-
-Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following acknowledgments and
-disclaimers.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-3. The names "Carnegie Mellon University," "SEI" and/or "Software
-Engineering Institute" shall not be used to endorse or promote
-products derived from this software without prior written
-permission. For written permission, please contact
-[email protected].
-
-4. Products derived from this software may not be called "SEI" nor may
-"SEI" appear in their names without prior written permission of
-[email protected].
-
-5. Redistributions of any form whatsoever must retain the following
-acknowledgment:
-
-This material is based upon work funded and supported by the
-Department of Defense under Contract No. FA8721-05-C-0003 with
-Carnegie Mellon University for the operation of the Software
-Engineering Institute, a federally funded research and development
-center.
-
-Any opinions, findings and conclusions or recommendations expressed in
-this material are those of the author(s) and do not necessarily
-reflect the views of the United States Department of Defense.
-
-NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
-INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
-UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
-IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
-FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
-OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
-MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
-TRADEMARK, OR COPYRIGHT INFRINGEMENT.
-
-This material has been approved for public release and unlimited
-distribution.
-
-DM-0000575
-
-**********************************************************************/
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
 
 /* Generated by CIL v. 1.6.0 */
 /* print_CIL_Input is true */

c/seq-mthreaded/pals_STARTPALS_ActiveStandby.1.ufo.UNBOUNDED.pals.c

@@ -2,60 +2,13 @@ extern void abort(void);
 extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
 void reach_error() { __assert_fail("0", "pals_STARTPALS_ActiveStandby.1.ufo.UNBOUNDED.pals.c", 3, "reach_error"); }
 
-/**********************************************************************
-
-Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following acknowledgments and
-disclaimers.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-3. The names "Carnegie Mellon University," "SEI" and/or "Software
-Engineering Institute" shall not be used to endorse or promote
-products derived from this software without prior written
-permission. For written permission, please contact
-[email protected].
-
-4. Products derived from this software may not be called "SEI" nor may
-"SEI" appear in their names without prior written permission of
-[email protected].
-
-5. Redistributions of any form whatsoever must retain the following
-acknowledgment:
-
-This material is based upon work funded and supported by the
-Department of Defense under Contract No. FA8721-05-C-0003 with
-Carnegie Mellon University for the operation of the Software
-Engineering Institute, a federally funded research and development
-center.
-
-Any opinions, findings and conclusions or recommendations expressed in
-this material are those of the author(s) and do not necessarily
-reflect the views of the United States Department of Defense.
-
-NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
-INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
-UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
-IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
-FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
-OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
-MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
-TRADEMARK, OR COPYRIGHT INFRINGEMENT.
-
-This material has been approved for public release and unlimited
-distribution.
-
-DM-0000575
-
-**********************************************************************/
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
 
 /* Generated by CIL v. 1.6.0 */
 /* print_CIL_Input is true */

c/seq-mthreaded/pals_STARTPALS_ActiveStandby.4_1.ufo.BOUNDED-10.pals.c

@@ -2,60 +2,13 @@ extern void abort(void);
 extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
 void reach_error() { __assert_fail("0", "pals_STARTPALS_ActiveStandby.4_1.ufo.BOUNDED-10.pals.c", 3, "reach_error"); }
 
-/**********************************************************************
-
-Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following acknowledgments and
-disclaimers.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-3. The names "Carnegie Mellon University," "SEI" and/or "Software
-Engineering Institute" shall not be used to endorse or promote
-products derived from this software without prior written
-permission. For written permission, please contact
-[email protected].
-
-4. Products derived from this software may not be called "SEI" nor may
-"SEI" appear in their names without prior written permission of
-[email protected].
-
-5. Redistributions of any form whatsoever must retain the following
-acknowledgment:
-
-This material is based upon work funded and supported by the
-Department of Defense under Contract No. FA8721-05-C-0003 with
-Carnegie Mellon University for the operation of the Software
-Engineering Institute, a federally funded research and development
-center.
-
-Any opinions, findings and conclusions or recommendations expressed in
-this material are those of the author(s) and do not necessarily
-reflect the views of the United States Department of Defense.
-
-NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
-INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
-UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
-IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
-FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
-OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
-MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
-TRADEMARK, OR COPYRIGHT INFRINGEMENT.
-
-This material has been approved for public release and unlimited
-distribution.
-
-DM-0000575
-
-**********************************************************************/
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
 
 /* Generated by CIL v. 1.6.0 */
 /* print_CIL_Input is true */

c/seq-mthreaded/pals_STARTPALS_ActiveStandby.4_1.ufo.UNBOUNDED.pals.c

@@ -2,60 +2,13 @@ extern void abort(void);
 extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
 void reach_error() { __assert_fail("0", "pals_STARTPALS_ActiveStandby.4_1.ufo.UNBOUNDED.pals.c", 3, "reach_error"); }
 
-/**********************************************************************
-
-Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following acknowledgments and
-disclaimers.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-3. The names "Carnegie Mellon University," "SEI" and/or "Software
-Engineering Institute" shall not be used to endorse or promote
-products derived from this software without prior written
-permission. For written permission, please contact
-[email protected].
-
-4. Products derived from this software may not be called "SEI" nor may
-"SEI" appear in their names without prior written permission of
-[email protected].
-
-5. Redistributions of any form whatsoever must retain the following
-acknowledgment:
-
-This material is based upon work funded and supported by the
-Department of Defense under Contract No. FA8721-05-C-0003 with
-Carnegie Mellon University for the operation of the Software
-Engineering Institute, a federally funded research and development
-center.
-
-Any opinions, findings and conclusions or recommendations expressed in
-this material are those of the author(s) and do not necessarily
-reflect the views of the United States Department of Defense.
-
-NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
-INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
-UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
-IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
-FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
-OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
-MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
-TRADEMARK, OR COPYRIGHT INFRINGEMENT.
-
-This material has been approved for public release and unlimited
-distribution.
-
-DM-0000575
-
-**********************************************************************/
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
 
 /* Generated by CIL v. 1.6.0 */
 /* print_CIL_Input is true */

c/seq-mthreaded/pals_STARTPALS_ActiveStandby.4_2.ufo.BOUNDED-10.pals.c

@@ -2,60 +2,13 @@ extern void abort(void);
 extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
 void reach_error() { __assert_fail("0", "pals_STARTPALS_ActiveStandby.4_2.ufo.BOUNDED-10.pals.c", 3, "reach_error"); }
 
-/**********************************************************************
-
-Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following acknowledgments and
-disclaimers.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-3. The names "Carnegie Mellon University," "SEI" and/or "Software
-Engineering Institute" shall not be used to endorse or promote
-products derived from this software without prior written
-permission. For written permission, please contact
-[email protected].
-
-4. Products derived from this software may not be called "SEI" nor may
-"SEI" appear in their names without prior written permission of
-[email protected].
-
-5. Redistributions of any form whatsoever must retain the following
-acknowledgment:
-
-This material is based upon work funded and supported by the
-Department of Defense under Contract No. FA8721-05-C-0003 with
-Carnegie Mellon University for the operation of the Software
-Engineering Institute, a federally funded research and development
-center.
-
-Any opinions, findings and conclusions or recommendations expressed in
-this material are those of the author(s) and do not necessarily
-reflect the views of the United States Department of Defense.
-
-NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
-INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
-UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
-IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
-FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
-OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
-MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
-TRADEMARK, OR COPYRIGHT INFRINGEMENT.
-
-This material has been approved for public release and unlimited
-distribution.
-
-DM-0000575
-
-**********************************************************************/
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
+// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
 
 /* Generated by CIL v. 1.6.0 */
 /* print_CIL_Input is true */