summaryrefslogtreecommitdiff
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
diff options
context:
space:
mode:
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h')
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h16
1 files changed, 16 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
new file mode 100644
index 000000000000..a64955447995
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/assume.h
@@ -0,0 +1,16 @@
+#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