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 18