summaryrefslogtreecommitdiff
path: root/tools/testing/selftests/rcutorture
diff options
context:
space:
mode:
authorIngo Molnar <mingo@kernel.org>2017-11-07 12:32:44 +0300
committerIngo Molnar <mingo@kernel.org>2017-11-07 12:32:44 +0300
commit8c5db92a705d9e2c986adec475980d1120fa07b4 (patch)
tree9f0eea56889819707c0a1a8eb5b1fb2db3cdaf3d /tools/testing/selftests/rcutorture
parentca5d376e17072c1b60c3fee66f3be58ef018952d (diff)
parente4880bc5dfb1f02b152e62a894b5c6f3e995b3cf (diff)
downloadlinux-8c5db92a705d9e2c986adec475980d1120fa07b4.tar.xz
Merge branch 'linus' into locking/core, to resolve conflicts
Conflicts: include/linux/compiler-clang.h include/linux/compiler-gcc.h include/linux/compiler-intel.h include/uapi/linux/stddef.h Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/testing/selftests/rcutorture')
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h1
-rwxr-xr-xtools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile1
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c1
-rwxr-xr-xtools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh1
20 files changed, 20 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
index 16b01559fa55..4bed0b678f8b 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile
@@ -1,3 +1,4 @@
+# SPDX-License-Identifier: GPL-2.0
all: srcu.c store_buffering
LINUX_SOURCE = ../../../../../..
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
index 4a3d538fef12..891ad13e95b2 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
/*
* This header has been modifies to remove definitions of types that
* are defined in standard userspace headers or are problematic for some
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
index c9e8bc5082a7..e05182d3e47d 100755
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk
@@ -1,4 +1,5 @@
#!/usr/bin/awk -f
+# SPDX-License-Identifier: GPL-2.0
# Modify SRCU for formal verification. The first argument should be srcu.h and
# the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
index a64955447995..570a49d9da7e 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef ASSUME_H
#define ASSUME_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
index cc27b9ebcf20..3f95a768a03b 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/barriers.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef BARRIERS_H
#define BARRIERS_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
index 2a80e91f78e7..5e7912c6a521 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef BUG_ON_H
#define BUG_ON_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
index 29eb5d2697ed..e67ee5b3dd7c 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <config.h>
/* Include all source files. */
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
index a60038aeea7a..283d7103334f 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/config.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
/* "Cheater" definitions based on restricted Kconfig choices. */
#undef CONFIG_TINY_RCU
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
index 5ec582a53018..e5202d4cff30 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <config.h>
#include <assert.h>
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
index 3aad63917858..0dd27aa517a7 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/int_typedefs.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef INT_TYPEDEFS_H
#define INT_TYPEDEFS_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
index 356004665576..cf6938d679d7 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef LOCKS_H
#define LOCKS_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
index ca892e3b2351..9440cc39e3c6 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <config.h>
#include "misc.h"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
index 3de5a49de49b..27e67a3f291f 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef PERCPU_H
#define PERCPU_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
index 4f1b068e9b7a..b4083ae348fb 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <config.h>
#include "preempt.h"
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
index 2f95ee0e4dd5..f8b762cd214c 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef PREEMPT_H
#define PREEMPT_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c
index ac9cbc62b411..97f592048e0b 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <config.h>
#include <assert.h>
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
index e58c8dfd3e90..28b960300971 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h
@@ -1,3 +1,4 @@
+/* SPDX-License-Identifier: GPL-2.0 */
#ifndef WORKQUEUES_H
#define WORKQUEUES_H
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
index 3a3aee149225..ad21b925fbb4 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/Makefile
@@ -1,3 +1,4 @@
+# SPDX-License-Identifier: GPL-2.0
CBMC_FLAGS = -I../.. -I../../src -I../../include -I../../empty_includes -32 -pointer-check -mm pso
all:
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c
index 470b1105a112..2ce2016f7871 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/test.c
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: GPL-2.0
#include <src/combined_source.c>
int x;
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
index d1545972a0fa..2fe1f0339b4f 100755
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
@@ -1,4 +1,5 @@
#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0
# This script expects a mode (either --should-pass or --should-fail) followed by
# an input file. The script uses the following environment variables. The test C
generated by cgit v1.2.3 (git 2.39.0) at 2024-12-29 22:55:45 +0300