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