diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal')
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 16b0155..4bed0b6 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 4a3d538..891ad13 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 c9e8bc5..e05182d 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 a649554..570a49d 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 6687acc..be3fdd3 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 2a80e91..5e7912c 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 29eb5d26..e67ee5b 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 a60038a..283d710 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 5ec582a..e5202d4 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 3aad639..0dd27aa 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 3560046..cf6938d 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 ca892e3..9440cc3 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 3de5a49..27e67a3 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 4f1b068..b4083ae 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 2f95ee0..f8b762c 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 ac9cbc6..97f5920 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 e58c8df..28b9603 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 3a3aee1..ad21b92 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 470b110..2ce2016 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 d154597..2fe1f03 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 |
