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