/* SPDX-License-Identifier: GPL-2.0 */
#ifndef ASSUME_H
#define ASSUME_H

/* Provide an assumption macro that can be disabled for gcc. */
#ifdef RUN
#define assume(x) \
	do { \
		/* Evaluate x to suppress warnings. */ \
		(void) (x); \
	} while (0)

#else
#define assume(x) __CPROVER_assume(x)
#endif

#endif