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

#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
100.00%
1
100.00%
Total
33
100.00%
1
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.