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