root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/include_srcu.c

   1 // SPDX-License-Identifier: GPL-2.0
   2 #include <config.h>
   3 
   4 #include <assert.h>
   5 #include <errno.h>
   6 #include <inttypes.h>
   7 #include <pthread.h>
   8 #include <stddef.h>
   9 #include <string.h>
  10 #include <sys/types.h>
  11 
  12 #include "int_typedefs.h"
  13 
  14 #include "barriers.h"
  15 #include "bug_on.h"
  16 #include "locks.h"
  17 #include "misc.h"
  18 #include "preempt.h"
  19 #include "percpu.h"
  20 #include "workqueues.h"
  21 
  22 #ifdef USE_SIMPLE_SYNC_SRCU
  23 #define synchronize_srcu(sp) synchronize_srcu_original(sp)
  24 #endif
  25 
  26 #include <srcu.c>
  27 
  28 #ifdef USE_SIMPLE_SYNC_SRCU
  29 #undef synchronize_srcu
  30 
  31 #include "simple_sync_srcu.c"
  32 #endif