tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h

   1 #ifndef ASSUME_H
   2 #define ASSUME_H
   3
   4 /* Provide an assumption macro that can be disabled for gcc. */
   5 #ifdef RUN
   6 #define assume(x) \
   7         do { \
   8                 /* Evaluate x to suppress warnings. */ \
   9                 (void) (x); \
  10         } while (0)
  11
  12 #else
  13 #define assume(x) __CPROVER_assume(x)
  14 #endif
  15
  16 #endif