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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
/*-----------------------------------------------------------------------
File : cio_output.c
Author: Stephan Schulz
Contents
Simple functions for secure opening of output files with -
convention and error checking. Much simpler than the input, because
much less can go wrong with output...
Copyright 1998, 1999 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details..
Run "eprover -h" for contact information.
Changes
<1> Fri Nov 28 11:55:59 MET 1997
New
-----------------------------------------------------------------------*/
#include <cio_output.h>
/*---------------------------------------------------------------------*/
/* Global Variables */
/*---------------------------------------------------------------------*/
long OutputLevel = 1;
FILE* GlobalOut;
int GlobalOutFD = STDOUT_FILENO;
/*---------------------------------------------------------------------*/
/* Forward Declarations */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Internal Functions */
/*---------------------------------------------------------------------*/
/*---------------------------------------------------------------------*/
/* Exported Functions */
/*---------------------------------------------------------------------*/
/*-----------------------------------------------------------------------
//
// Function: OpenGlobalOut()
//
// Set GobalOut to a FILE* connected to file outname, set
// GlobalOutFD accordingly.
//
// Global Variables: GlobalOut, GlobalOutFD
//
// Side Effects : As above.
//
/----------------------------------------------------------------------*/
void OpenGlobalOut(char* outname)
{
GlobalOut = OutOpen(outname);
GlobalOutFD = fileno(GlobalOut);
}
/*-----------------------------------------------------------------------
//
// Function: OutOpen()
//
// Open a file for writing and return it, with error checking. "-"
// and NULL are both taken to mean stdout.
//
// Global Variables: -
//
// Side Effects : Opens file
//
/----------------------------------------------------------------------*/
FILE* OutOpen(char* name)
{
FILE* out;
if(name && strcmp(name,"-")!= 0)
{
VERBOUTARG("Output file is ", name);
if(! (out = fopen(name,"w")))
{
TmpErrno = errno; /* Save error number, the following call to
sprintf() can theoretically alter the
value !*/
sprintf(ErrStr, "Cannot open file %s", name);
SysError(ErrStr, FILE_ERROR);
}
}
else
{
VERBOUT("Output is going to <stdout>\n");
out = stdout;
}
clearerr(out);
return out;
}
/*-----------------------------------------------------------------------
//
// Function: OutClose()
//
// Close the file, checking for errors. If stdout, just flush
// it. Error messages are bound to be short, but errors should only
// result from program errors or extremely obscure circumstances.
//
// Global Variables: -
//
// Side Effects : Closes file
//
/----------------------------------------------------------------------*/
void OutClose(FILE* file)
{
fflush(file);
if(ferror(file))
{
Error("Output stream to be closed reports error (probably "
"broken pipe, file system full or quota exceeded)",
FILE_ERROR);
}
VERBOUT("Closing output\n");
if(file != stdout)
{
if(fclose(file) != 0)
{
TmpErrno = errno;
SysError("Error while closing file", FILE_ERROR);
}
}
}
/*-----------------------------------------------------------------------
//
// Function: PrintDashedStatuses()
//
// This is a weird simple thing needed far above. If stat1 and stat2
// are NULL, print fallback. If either is non-NULL, print it. If both
// are non-NULL, print them both separated by a dash.
//
// Global Variables: -
//
// Side Effects : Output
//
/----------------------------------------------------------------------*/
void PrintDashedStatuses(FILE* out, char* stat1, char* stat2, char* fallback)
{
assert(fallback);
if(stat1 && stat2)
{
fprintf(out, "%s-%s", stat1, stat2);
}
else if(stat1)
{
fputs(stat1, out);
}
else if(stat2)
{
fputs(stat2, out);
}
else
{
fputs(fallback, out);
}
}
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
