blob: 570a49d9da7e2bbd6237bc80d3ee758f02aacb53 (
plain)
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
|