LXR linux/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
  17