[people/arne_f/kernel.git] / tools / testing / selftests / rcutorture / formal / srcu-cbmc / src / assume.h

/* 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
Commit	Line	Data
b2441318	1	/* SPDX-License-Identifier: GPL-2.0 */
418b2977 LR	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