SPIN_LOCK_UNLOCKED  128 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h #define __SPIN_LOCK_UNLOCKED(x) SPIN_LOCK_UNLOCKED
SPIN_LOCK_UNLOCKED  129 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h #define DEFINE_SPINLOCK(x) spinlock_t x = SPIN_LOCK_UNLOCKED