diff options
| -rw-r--r-- | lib/Makefile | 4 | ||||
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/lib/Makefile b/lib/Makefile index d11c48ec8ffd..f242a92eefd3 100644 --- a/lib/Makefile +++ b/lib/Makefile @@ -72,9 +72,13 @@ CFLAGS_kobject.o += -DDEBUG CFLAGS_kobject_uevent.o += -DDEBUG endif + obj-$(CONFIG_DEBUG_INFO_REDUCED) += debug_info.o CFLAGS_debug_info.o += $(call cc-option, -femit-struct-debug-detailed=any) +CFLAGS_vsprintf.o += -O0 +CFLAGS_asprintf.o += -O0 + obj-$(CONFIG_GENERIC_IOMAP) += iomap.o obj-$(CONFIG_GENERIC_PCI_IOMAP) += pci_iomap.o obj-$(CONFIG_HAS_IOMEM) += iomap_copy.o devres.o 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 6798ab45032d..e05182d3e47d 100644 --- 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,4 @@ -#!/usr/usr/bin/awk -f +#!/usr/bin/awk -f # SPDX-License-Identifier: GPL-2.0 # Modify SRCU for formal verification. The first argument should be srcu.h and |