spot 2.16
Loading...
Searching...
No Matches
common.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3//
4// This file is part of Spot, a model checking library.
5//
6// Spot is free software; you can redistribute it and/or modify it
7// under the terms of the GNU General Public License as published by
8// the Free Software Foundation; either version 3 of the License, or
9// (at your option) any later version.
10//
11// Spot is distributed in the hope that it will be useful, but WITHOUT
12// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14// License for more details.
15//
16// You should have received a copy of the GNU General Public License
17// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19#include <cstdlib>
20#include <stdexcept>
21#include <cassert>
22
23#pragma once
24
25#ifdef __GNUC__
26#define SPOT_LIKELY(expr) __builtin_expect(!!(expr), 1)
27#define SPOT_UNLIKELY(expr) __builtin_expect(!!(expr), 0)
28#else
29#define SPOT_LIKELY(expr) (expr)
30#define SPOT_UNLIKELY(expr) (expr)
31#endif
32
33#ifdef SWIG
34 #define SPOT_DEPRECATED(msg)
35 #define SPOT_FALLTHROUGH
36#else
37 #if __cplusplus < 201703L
38 #error C++17 compiler required
39 #endif
40 #define SPOT_DEPRECATED(msg) [[deprecated(msg)]]
41 #define SPOT_FALLTHROUGH [[fallthrough]]
42#endif
43
44#if defined _WIN32 || defined __CYGWIN__
45 #define SPOT_HELPER_DLL_IMPORT __declspec(dllimport)
46 #define SPOT_HELPER_DLL_EXPORT __declspec(dllexport)
47 #define SPOT_HELPER_DLL_LOCAL
48#else
49 #if __GNUC__ >= 4
50 #define SPOT_HELPER_DLL_IMPORT __attribute__ ((visibility ("default")))
51 #define SPOT_HELPER_DLL_EXPORT __attribute__ ((visibility ("default")))
52 #define SPOT_HELPER_DLL_LOCAL __attribute__ ((visibility ("hidden")))
53 #else
54 #define SPOT_HELPER_DLL_IMPORT
55 #define SPOT_HELPER_DLL_EXPORT
56 #define SPOT_HELPER_DLL_LOCAL
57 #endif
58#endif
59
60#ifdef SPOT_BUILD
61 #define SPOT_DLL
62#endif
63
64
65// We should not call assert() in headers. For the rare cases where
66// we do really want to call assert(), use spot_assert__ instead.
67// Else use SPOT_ASSERT so the assert() are removed from user's
68// builds.
69#define spot_assert__ assert
70#if defined(SPOT_BUILD) || defined(SPOT_DEBUG)
71 #define SPOT_ASSERT(x) spot_assert__(x)
72#else
73 // Do not replace by SPOT_ASSUME(x), as x can have some costly
74 // side-effects we do not want to pay outside of debug mode.
75 #define SPOT_ASSERT(x) while (0)
76#endif
77
78// SPOT_API is used for the public API symbols. It either DLL imports
79// or DLL exports (or does nothing for static build) SPOT_LOCAL is
80// used for non-api symbols that may occur in header files.
81#ifdef SPOT_DLL
82 #ifdef SPOT_BUILD
83 #define SPOT_API SPOT_HELPER_DLL_EXPORT
84 #else
85 #define SPOT_API SPOT_HELPER_DLL_IMPORT
86 #endif
87 #define SPOT_LOCAL SPOT_HELPER_DLL_LOCAL
88#else
89 #define SPOT_API
90 #define SPOT_LOCAL
91#endif
92#define SPOT_API_VAR extern SPOT_API
93
94
95// Swig 3.0.2 does not understand 'final' when used
96// at class definition.
97#ifdef SWIG
98 #define final
99#endif
100
101
102// Do not use those in code, prefer SPOT_UNREACHABLE() instead.
103#if defined __clang__ || defined __GNUC__
104# define SPOT_UNREACHABLE_BUILTIN() __builtin_unreachable()
105# elif defined _MSC_VER
106# define SPOT_UNREACHABLE_BUILTIN() __assume(0)
107# else
108# define SPOT_UNREACHABLE_BUILTIN() abort()
109#endif
110
111// The extra parentheses in assert() is so that this
112// pattern is not caught by the style checker.
113#define SPOT_UNREACHABLE() do { \
114 SPOT_ASSERT(!("unreachable code reached")); \
115 SPOT_UNREACHABLE_BUILTIN(); \
116 } while (0)
117
118#define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented");
119
120
121#if SPOT_DEBUG && !defined(NDEBUG)
122#define SPOT_ASSUME(cond) assert(cond)
123#else
124#define SPOT_ASSUME(cond) \
125 do \
126 { \
127 if (!(cond)) \
128 SPOT_UNREACHABLE_BUILTIN(); \
129 } \
130 while (0)
131#endif
132
133
134// Useful when forwarding methods such as:
135// auto func(int param) SPOT_RETURN(implem_.func(param));
136#define SPOT_RETURN(code) -> decltype(code) { return code; }
137
138namespace spot
139{
141 struct SPOT_API parse_error: public std::runtime_error
142 {
144 parse_error(const std::string& s)
145 : std::runtime_error(s)
146 {
147 }
148 };
149
156 class SPOT_API parallel_policy
157 {
158 unsigned nthreads_;
159 public:
161 parallel_policy(unsigned nthreads = 1) : nthreads_(nthreads)
162 {
163 }
164
166 unsigned nthreads() const
167 {
168 return nthreads_;
169 }
170 };
171
172}
173
174// This is a workaround for the issue described in GNU GCC bug 89303.
175// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=89303
176//
177// In brief: with some version of gcc distributed by Debian unstable
178// and that correspond to something a bit newer than 8.2.1 (Debian is
179// tracking the gcc-8-branch instead of following releases), mixing
180// make_shared with enable_shared_from_this produces memory leaks or
181// bad_weak_ptr exceptions.
182//
183// Our workaround is simply to avoid calling make_shared in those
184// cases.
185//
186// The use of "enabled" in the macro name is just here to remember
187// that we only need this macro for classes that inherit from
188// enable_shared_from_this.
189#if __GNUC__ == 8 && __GNUC_MINOR__ == 2
190# define SPOT_make_shared_enabled__(TYPE, ...) \
191 std::shared_ptr<TYPE>(new TYPE(__VA_ARGS__))
192#else
193# define SPOT_make_shared_enabled__(TYPE, ...) \
194 std::make_shared<TYPE>(__VA_ARGS__)
195#endif
This class is used to tell parallel algorithms what resources they may use.
Definition common.hh:157
unsigned nthreads() const
Return the number of threads.
Definition common.hh:166
parallel_policy(unsigned nthreads=1)
Construct with nthreads threads.
Definition common.hh:161
Definition automata.hh:26
Exception thrown when a parse error is encountered.
Definition common.hh:142
parse_error(const std::string &s)
Construct with error message s.
Definition common.hh:144

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.8