ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
compiler_defs.h
Go to the documentation of this file.
1
#pragma once
2
4
/* Warnings / Diagnostics related
5
These warnings come from Clang, so it might
6
have a slight difference between Clang 11 and 14 warnings
7
*/
8
#if defined(_MSC_VER)
9
# define CC_DIAGNOSTIC_PUSH() __pragma(warning(push))
10
# define CC_DIAGNOSTIC_POP() __pragma(warning(pop))
11
# define CC_DIAGNOSTIC_DISABLE(x) __pragma(warning(disable : x))
12
13
// NOTE: The magic numbers came directly from MSVC
14
# define CC_DIAGNOSTIC_IGNORE_LLVM_CHECKS() \
15
__pragma(message("Disabling diagnostic checks for clang headers")) \
16
CC_DIAGNOSTIC_DISABLE(4146 4244 4267 4291 4624)
17
# define CC_DIAGNOSTIC_IGNORE_DEPRECATED_LITERAL_OPERATOR()
18
#else
19
# define CC_DIAGNOSTIC_PUSH() _Pragma("GCC diagnostic push")
20
# define CC_DIAGNOSTIC_POP() _Pragma("GCC diagnostic pop")
21
# define DO_PRAGMA(x) _Pragma(#x)
22
23
# define CC_DIAGNOSTIC_IGNORE_LLVM_CHECKS() \
24
DO_PRAGMA(GCC diagnostic ignored "-Wstrict-aliasing") \
25
DO_PRAGMA(GCC diagnostic ignored "-Wunused-parameter") \
26
DO_PRAGMA(GCC diagnostic ignored "-Wnonnull") \
27
DO_PRAGMA(GCC diagnostic ignored "-Wdeprecated-declarations") \
28
CC_DIAGNOSTIC_IGNORE_CLASS_MEMACCESS()
29
30
// -Wclass-memaccess is GCC-only; Clang does not recognise it and would emit
31
// -Wunknown-warning-option on the pragma itself.
32
# if defined(__GNUC__) && !defined(__clang__)
33
# define CC_DIAGNOSTIC_IGNORE_CLASS_MEMACCESS() \
34
DO_PRAGMA(GCC diagnostic ignored "-Wclass-memaccess")
35
# else
36
# define CC_DIAGNOSTIC_IGNORE_CLASS_MEMACCESS()
37
# endif
38
39
// -Wdeprecated-literal-operator exists only on Clang >= 17 and GCC >= 15;
40
// emitting the pragma on older compilers trips -Wunknown-warning-option
41
// (Clang) or -Wpragmas (GCC). Probe with Clang's __has_warning where
42
// available, and fall back to a GCC version check otherwise.
43
# if defined(__has_warning)
44
# if __has_warning("-Wdeprecated-literal-operator")
45
# define CC_DIAGNOSTIC_IGNORE_DEPRECATED_LITERAL_OPERATOR() \
46
DO_PRAGMA(GCC diagnostic ignored "-Wdeprecated-literal-operator")
47
# else
48
# define CC_DIAGNOSTIC_IGNORE_DEPRECATED_LITERAL_OPERATOR()
49
# endif
50
# elif defined(__GNUC__) && __GNUC__ >= 15
51
# define CC_DIAGNOSTIC_IGNORE_DEPRECATED_LITERAL_OPERATOR() \
52
DO_PRAGMA(GCC diagnostic ignored "-Wdeprecated-literal-operator")
53
# else
54
# define CC_DIAGNOSTIC_IGNORE_DEPRECATED_LITERAL_OPERATOR()
55
# endif
56
#endif
57
58
#ifndef GNUC_PREREQ
59
60
# if defined(__GNUC__) && defined(__GNUC_MINOR__) && \
61
defined(__GNUC_PATCHLEVEL__)
62
63
# define GNUC_PREREQ(maj, min, patch) \
64
((__GNUC__ << 20) + (__GNUC_MINOR__ << 10) + __GNUC_PATCHLEVEL__ >= \
65
((maj) << 20) + ((min) << 10) + (patch))
66
67
# elif defined(__GNUC__) && defined(__GNUC_MINOR__)
68
69
# define GNUC_PREREQ(maj, min, patch) \
70
((__GNUC__ << 20) + (__GNUC_MINOR__ << 10) >= \
71
((maj) << 20) + ((min) << 10))
72
73
# else
74
75
# define GNUC_PREREQ(maj, min, patch) 0
76
77
# endif
78
#endif
79
80
#if defined(_MSC_VER)
81
# define ATTRIBUTE_NOINLINE __declspec(noinline)
82
#elif __has_attribute(noinline) || GNUC_PREREQ(3, 4, 0)
83
# define ATTRIBUTE_NOINLINE __attribute__((noinline))
84
#else
85
# define ATTRIBUTE_NOINLINE
86
#endif
87
88
#define ATTRIBUTE_USED
89
#ifndef _MSC_VER
90
# if GNUC_PREREQ(3, 1, 0) || __has_attribute(used)
91
# undef ATTRIBUTE_USED
92
# define ATTRIBUTE_USED __attribute__((__used__))
93
# endif
94
#endif
95
96
#if !defined(NDEBUG)
97
# define DUMP_METHOD ATTRIBUTE_NOINLINE ATTRIBUTE_USED
98
#else
99
# define DUMP_METHOD ATTRIBUTE_NOINLINE
100
#endif
src
util
base
compiler_defs.h
Generated by
1.15.0