1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
/********************* */
/*! \file safe_print.h
** \verbatim
** Top contributors (to current version):
** Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Print functions that are safe to use in a signal handler.
**
** Signal handlers only allow a very limited set of operations, e.g. dynamic
** memory allocation is not possible. This set of functions can be used to
** print information from a signal handler.
**
** The safe_print function takes a template parameter T and prints an argument
** of type const T& to avoid copying, e.g. when printing std::strings. For
** consistency, we also pass primitive types by reference (otherwise, functions
** in statistics_registry.h would require specialization or we would have to
** use function overloading).
**
** This header is a "cvc4_private_library.h" header because it is private but
** the safe_print functions are used in the driver. See also the description
** of "statistics_registry.h" for more information on
** "cvc4_private_library.h".
**/
#include "cvc4_private_library.h"
#ifndef CVC4__SAFE_PRINT_H
#define CVC4__SAFE_PRINT_H
#if __cplusplus >= 201103L
// For c++11 and newer
#include <cstdint>
#else
#include <stdint.h>
#endif
#include <unistd.h>
#include "lib/clock_gettime.h"
#include "util/result.h"
namespace CVC4 {
/**
* Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
* signal handler.
*/
template <size_t N>
void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
ssize_t nb = N - 1;
if (write(fd, msg, nb) != nb) {
abort();
}
}
/** Prints a variable of type T. Safe to use in a signal handler. */
template <typename T>
void CVC4_PUBLIC safe_print(int fd, const T& msg) {
safe_print(fd, "<unsupported>");
}
template <>
void CVC4_PUBLIC safe_print(int fd, const std::string& msg);
template <>
void CVC4_PUBLIC safe_print(int fd, const int64_t& _i);
template <>
void CVC4_PUBLIC safe_print(int fd, const int32_t& i);
template <>
void CVC4_PUBLIC safe_print(int fd, const uint64_t& _i);
template <>
void CVC4_PUBLIC safe_print(int fd, const uint32_t& i);
template <>
void CVC4_PUBLIC safe_print(int fd, const double& _d);
template <>
void CVC4_PUBLIC safe_print(int fd, const float& f);
template <>
void CVC4_PUBLIC safe_print(int fd, const bool& b);
template <>
void CVC4_PUBLIC safe_print(int fd, void* const& addr);
template <>
void CVC4_PUBLIC safe_print(int fd, const timespec& t);
/** Prints an integer in hexadecimal. Safe to use in a signal handler. */
void safe_print_hex(int fd, uint64_t i);
/**
* Prints a right aligned number. Fills up remaining space with zeros. Safe to
* use in a signal handler.
*/
void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
} /* CVC4 namespace */
#endif /* CVC4__SAFE_PRINT_H */
|
