aboutsummaryrefslogtreecommitdiffstats
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
diff options
context:
space:
mode:
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h')
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
index d27285f8ee82..8bc960e5e713 100644
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/types.h
@@ -59,11 +59,7 @@ typedef __u32 uint32_t;
*
* blkcnt_t is the type of the inode's block count.
*/
-#ifdef CONFIG_LBDAF
typedef u64 sector_t;
-#else
-typedef unsigned long sector_t;
-#endif
/*
* The type of an index into the pagecache.