tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

/* 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