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