diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk')
| -rwxr-xr-x | tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 1 |
1 files changed, 1 insertions, 0 deletions
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 |