diff options
Diffstat (limited to '')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c | 32 |
1 files changed, 0 insertions, 32 deletions
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 deleted file mode 100644 index e5202d4cff30..000000000000 --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c +++ /dev/null @@ -1,32 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <config.h> - -#include <assert.h> -#include <errno.h> -#include <inttypes.h> -#include <pthread.h> -#include <stddef.h> -#include <string.h> -#include <sys/types.h> - -#include "int_typedefs.h" - -#include "barriers.h" -#include "bug_on.h" -#include "locks.h" -#include "misc.h" -#include "preempt.h" -#include "percpu.h" -#include "workqueues.h" - -#ifdef USE_SIMPLE_SYNC_SRCU -#define synchronize_srcu(sp) synchronize_srcu_original(sp) -#endif - -#include <srcu.c> - -#ifdef USE_SIMPLE_SYNC_SRCU -#undef synchronize_srcu - -#include "simple_sync_srcu.c" -#endif |