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

/* [<][>][^][v][top][bottom][index][help] */

INCLUDED FROM

   1 /* SPDX-License-Identifier: GPL-2.0 */
   2 #ifndef ASSUME_H
   3 #define ASSUME_H
   4 
   5 /* Provide an assumption macro that can be disabled for gcc. */
   6 #ifdef RUN
   7 #define assume(x) \
   8         do { \
   9                 /* Evaluate x to suppress warnings. */ \
  10                 (void) (x); \
  11         } while (0)
  12 
  13 #else
  14 #define assume(x) __CPROVER_assume(x)
  15 #endif
  16 
  17 #endif
/* [<][>][^][v][top][bottom][index][help] */