Release 4.15 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
Overall Contributors
Person
Tokens
Prop
Commits
CommitProp
Lance Roy
33
97.06%
1
50.00%
Greg Kroah-Hartman
1
2.94%
1
50.00%
Total
34
100.00%
2
100.00%
Directory: tools/testing/selftests/rcutorture/formal/srcu-cbmc/src

Information contained on this website is for historical information purposes only and does not indicate or represent copyright ownership.