diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile')
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile new file mode 100644 index 000000000000..16b01559fa55 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/Makefile @@ -0,0 +1,16 @@ +all: srcu.c store_buffering + +LINUX_SOURCE = ../../../../../.. + +modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \ + $(LINUX_SOURCE)/kernel/rcu/srcu.c + +modified_srcu_output = include/linux/srcu.h srcu.c + +include/linux/srcu.h: srcu.c + +srcu.c: modify_srcu.awk Makefile $(modified_srcu_input) + awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output) + +store_buffering: + @cd tests/store_buffering; make |