diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src')
14 files changed, 14 insertions, 0 deletions
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 6687acc08e6d..be3fdd351937 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 |