[linux-block.git] / tools / testing / selftests / rcutorture / formal / srcu-cbmc / Makefile

# SPDX-License-Identifier: GPL-2.0
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
Commit	Line	Data
b2441318	1	# SPDX-License-Identifier: GPL-2.0
418b2977 LR	2	all: srcu.c store_buffering
	3
	4	LINUX_SOURCE = ../../../../../..
	5
	6	modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \
	7	$(LINUX_SOURCE)/kernel/rcu/srcu.c
	8
	9	modified_srcu_output = include/linux/srcu.h srcu.c
	10
	11	include/linux/srcu.h: srcu.c
	12
	13	srcu.c: modify_srcu.awk Makefile $(modified_srcu_input)
	14	awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output)
	15
	16	store_buffering:
	17	@cd tests/store_buffering; make