2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
10 extern bool /*@alt void@*/ check (bool p_x);
11 # define check(p_x) doCheck (p_x, cstring_fromChars (#p_x), cstring_makeLiteralTemp (__FILE__), __LINE__)
13 extern bool doCheck (bool p_x, cstring p_pred, cstring p_file, int p_line);
15 extern /*@noreturnwhenfalse@*/ void llassert (/*@sef@*/ bool p_test);
17 # define llassert(tst) \
19 if (context_getFlag (FLG_TRYTORECOVER)) checkParseError (); \
20 lldiagmsg (message ("%s:%d: at source point", \
21 cstring_makeLiteralTemp (__FILE__), __LINE__)); \
22 llbuglit ("llassert failed: " #tst); \
26 extern /*@noreturnwhenfalse@*/ void llassertretnull (/*@sef@*/ bool p_test);
27 # define llassertretnull(tst) \
29 if (context_getFlag (FLG_TRYTORECOVER)) checkParseError (); \
30 lldiagmsg (message ("%s:%d: at source point", \
31 cstring_makeLiteralTemp (__FILE__), __LINE__)); \
32 llbuglit ("llassert failed: " #tst); \
36 ** Use this for assertions in error-generation code (that
37 ** might lead to infinite loops of failed assertions if
38 ** the normal error generation routines are used).
41 extern /*@noreturnwhenfalse@*/ void llassertprotect (/*@sef@*/ bool p_test);
42 # define llassertprotect(tst) \
44 fprintf (stderr, "%s:%d: at source point: ", __FILE__, __LINE__); \
45 fprintf (stderr, "protected fatal llassert failed: " #tst "\n"); \
46 llexit (EXIT_FAILURE); \
49 extern /*@noreturnwhenfalse@*/ void llassertfatal (/*@sef@*/ bool p_test);
50 # define llassertfatal(tst) \
52 llfatalbug (message("%s:%d: fatal llassert failed: " #tst, \
53 cstring_makeLiteralTemp (__FILE__), __LINE__)); \
57 ** llassertprint and llassertprintret are in splintMacros.nf
60 extern void llmsg (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
62 extern void lldiagmsg (/*@only@*/ cstring p_s) /*@modifies stderr@*/ ;
63 extern void llmsgplain (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
64 extern void llhint (/*@only@*/ cstring p_s)
65 /*@globals g_currentloc, g_msgstream;@*/
66 /*@modifies g_msgstream@*/ ;
68 extern /*@private@*/ /*@noreturn@*/ void xllfatalbug (char *p_srcFile, int p_srcLine,
69 /*@only@*/ cstring p_s)
70 /*@globals g_currentloc@*/
71 /*@modifies stderr@*/ ;
73 extern /*@noreturn@*/ void llfatalbug (/*@only@*/ cstring p_s)
74 /*@globals g_currentloc@*/
75 /*@modifies stderr@*/ ;
76 # define llfatalbug(p_s) \
77 xllfatalbug (__FILE__, __LINE__, p_s)
79 extern /*@private@*/ bool xllgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
80 /*@only@*/ cstring p_s, fileloc p_fl)
81 /*@modifies g_msgstream@*/ ;
83 extern bool llgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_fl)
84 /*@modifies g_msgstream@*/ ;
85 # define llgenerror(p_o, p_s, p_fl) \
86 xllgenerror (__FILE__, __LINE__, p_o, p_s, p_fl)
88 extern /*@private@*/ bool
89 xllgenhinterror (char *p_srcFile, int p_srcLine,
90 flagcode p_o, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint,
92 /*@modifies g_msgstream@*/ ;
94 extern bool llgenhinterror (flagcode p_o, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint,
95 fileloc p_fl) /*@modifies g_msgstream@*/ ;
97 # define llgenhinterror(p_o, p_s, p_hint, p_fl) \
98 xllgenhinterror (__FILE__, __LINE__, p_o, p_s, p_hint, p_fl)
101 extern void llerror (flagcode p_o, /*@only@*/ cstring p_s)
102 /*@globals g_msgstream, g_currentloc@*/
103 /*@modifies g_msgstream@*/ ;
104 # define llerror(p_o, p_s) \
105 ((void) llgenerror (p_o, p_s, g_currentloc))
107 extern void llgenmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_msgstream@*/ ;
108 extern /*@noreturn@*/ void llfatalerror (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
109 extern /*@noreturn@*/ void llfatalerrorLoc (/*@only@*/ cstring p_s)
110 /*@globals g_currentloc@*/
111 /*@modifies stderr@*/ ;
112 extern void llparseerror (/*@only@*/ cstring p_s)
113 /*@globals g_msgstream, g_currentloc@*/
114 /*@modifies g_msgstream@*/ ;
117 extern /*@noreturn@*/ void lclplainfatalerror (/*@only@*/ cstring p_msg) /*@modifies g_msgstream@*/ ;
118 extern /*@noreturn@*/ void lclfatalbug (/*@temp@*/ char *p_msg) /*@modifies g_msgstream@*/ ;
119 extern int lclNumberErrors (void) /*@*/ ;
120 extern bool lclHadNewError (void) /*@modifies internalState@*/ ;
121 extern /*@noreturn@*/ void lclfatalerror (ltoken p_t, /*@only@*/ cstring p_msg);
123 extern void xlclerror (char *p_srcFile, int p_srcLine, ltoken p_t, /*@only@*/ cstring p_msg) ;
125 extern void lclerror (ltoken p_t, /*@only@*/ cstring p_msg);
126 # define lclerror(p_t,p_msg) \
127 xlclerror (__FILE__, __LINE__, p_t, p_msg)
129 extern void lclbug (/*@only@*/ cstring p_s);
130 extern void lclplainerror (/*@only@*/ cstring p_msg);
131 extern bool lclHadError (void);
132 extern void lclRedeclarationError (ltoken p_id);
135 extern void llerror_flagWarning (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
137 extern /*@noreturn@*/ void llbugaux (cstring p_file, int p_line, /*@only@*/ cstring p_s)
138 /*@globals g_msgstream, g_currentloc@*/
139 /*@modifies *g_msgstream@*/ ;
141 extern /*@noreturn@*/ void llbug (/*@only@*/ cstring p_s)
142 /*@globals g_msgstream, g_currentloc@*/
143 /*@modifies *g_msgstream@*/ ;
145 /* doesn't really exit, but don't mind errors if it doesn't */
146 # define llbug(s) llbugaux (cstring_makeLiteralTemp (__FILE__), __LINE__, s)
148 extern void llquietbugaux (/*@only@*/ cstring p_s, cstring, int) /*@modifies *g_msgstream@*/ ;
149 extern void llquietbug (/*@only@*/ cstring) /*@modifies *g_msgstream@*/ ;
150 # define llquietbug(s) llquietbugaux (s, cstring_makeLiteralTemp (__FILE__), __LINE__)
152 extern void llcontbug (/*@only@*/ cstring p_s) /*@modifies *g_msgstream@*/ ;
153 /* doesn't really exit, but don't mind errors if it doesn't */
154 # define llcontbug(s) (llbug (s))
156 extern void cleanupMessages (void)
157 /*@globals g_msgstream, g_currentloc;@*/
158 /*@modifies g_msgstream, internalState@*/ ;
161 ** Report error iff f1 and f2 are set.
165 xoptgenerror2 (char *p_srcFile, int p_srcLine,
166 flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
167 /*@modifies *g_msgstream, internalState@*/ ;
170 optgenerror2 (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
171 /*@modifies *g_msgstream, internalState@*/ ;
172 # define optgenerror2(p_f1, p_f2, p_s, p_loc) \
173 (xoptgenerror2 (__FILE__, __LINE__, p_f1, p_f2, p_s, p_loc))
176 ** Report error if f1 is set and f2 is not set.
180 xoptgenerror2n (char *p_srcFile, int p_srcLine,
181 flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
182 /*@modifies *g_msgstream, internalState@*/ ;
185 optgenerror2n (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
186 /*@modifies *g_msgstream, internalState@*/ ;
187 # define optgenerror2n(p_f1, p_f2, p_s, p_loc) \
188 (xoptgenerror2n (__FILE__, __LINE__, p_f1, p_f2, p_s, p_loc))
190 extern /*@private@*/ bool xlloptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
191 /*@modifies *g_msgstream, internalState@*/ ;
193 extern bool lloptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
194 /*@modifies *g_msgstream, internalState@*/ ;
195 # define lloptgenerror(p_o, p_s, p_loc) \
196 (xlloptgenerror (__FILE__, __LINE__, p_o, p_s, p_loc))
198 extern bool xllnoptgenerror (char *p_srcFile, int p_srcLine,
199 flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
200 /*@modifies *g_msgstream, internalState@*/ ;
202 extern bool llnoptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
203 /*@modifies *g_msgstream, internalState@*/ ;
204 # define llnoptgenerror(p_o, p_s, p_loc) \
205 (xllnoptgenerror (__FILE__, __LINE__, p_o, p_s, p_loc))
207 extern /*@private@*/ bool
208 xllgenformattypeerror (char *p_srcFile, int p_srcLine,
209 ctype p_t1, exprNode p_e1,
210 ctype p_t2, exprNode p_e2,
211 /*@only@*/ cstring p_s, fileloc p_fl)
212 /*@modifies *g_msgstream, internalState@*/ ;
214 extern bool llgenformattypeerror (ctype p_t1, exprNode p_e1,
215 ctype p_t2, exprNode p_e2,
216 /*@only@*/ cstring p_s, fileloc p_fl)
217 /*@modifies *g_msgstream, internalState@*/ ;
218 # define llgenformattypeerror(p_t1, p_e1, p_t2, p_e2, p_s, p_fl) \
219 xllgenformattypeerror (__FILE__, __LINE__, p_t1, p_e1, p_t2, p_e2, p_s, p_fl)
221 extern bool xllgentypeerror (char *p_srcFile, int p_srcLine,
222 ctype p_t1, exprNode p_e1,
223 ctype p_t2, exprNode p_e2,
224 /*@only@*/ cstring p_s,
226 /*@modifies *g_msgstream, internalState@*/ ;
228 extern bool llgentypeerror (ctype p_t1, exprNode p_e1,
229 ctype p_t2, exprNode p_e2,
230 /*@only@*/ cstring p_s,
232 /*@modifies *g_msgstream, internalState@*/ ;
233 # define llgentypeerror(p_t1, p_e1, p_t2, p_e2, p_s, p_fl) \
234 xllgentypeerror (__FILE__, __LINE__, p_t1, p_e1, p_t2, p_e2, p_s, p_fl)
236 extern bool gentypeerror (/*@sef@*/ ctype p_t1,
237 /*@sef@*/ exprNode p_e1,
238 /*@sef@*/ ctype p_t2,
239 /*@sef@*/ exprNode p_e2,
240 /*@sef@*/ /*@only@*/ cstring p_s,
241 /*@sef@*/ fileloc p_loc)
242 /*@modifies *g_msgstream, internalState@*/ ;
244 /*@-branchstate@*/ /* sef only s is freed on one branch */
245 #define gentypeerror(t1, e1, t2, e2, s, loc) \
246 (context_suppressFlagMsg (FLG_TYPE,loc) \
247 ? (flagcode_recordSuppressed (FLG_TYPE), FALSE) \
248 : llgentypeerror (t1, e1, t2, e2, s, loc))
252 ** These are macros to save evaluating s (which may be some expensive
253 ** message generation function).
257 optgenerror (/*@sef@*/ flagcode p_o, /*@sef@*/ /*@only@*/ cstring p_s,
258 /*@sef@*/ fileloc p_loc)
259 /*@modifies *g_msgstream, internalState@*/ ;
261 /*@-branchstate@*/ /* sef only s is freed on one branch */
262 #define optgenerror(o,s,loc) \
263 (context_suppressFlagMsg(o,loc) ? (flagcode_recordSuppressed(o), FALSE) \
264 : lloptgenerror (o, s, loc))
268 voptgenerror (/*@sef@*/ flagcode p_o, /*@sef@*/ /*@only@*/ cstring p_s,
269 /*@sef@*/ fileloc p_loc)
270 /*@modifies *g_msgstream, internalState@*/ ;
271 #define voptgenerror(o, s, loc) ((void) optgenerror(o,s,loc))
273 extern /*@private@*/ bool
274 xfsgenerror (char *p_srcFile, int p_srcLine,
275 flagSpec p_fs, /*@only@*/ cstring p_s, fileloc p_fl)
276 /*@modifies g_msgstream, internalState@*/ ;
278 extern bool fsgenerror (flagSpec p_fs, /*@only@*/ cstring p_s, fileloc p_fl)
279 /*@modifies g_msgstream, internalState@*/ ;
280 # define fsgenerror(p_fs, p_s, p_fl) \
281 xfsgenerror (__FILE__, __LINE__, p_fs, p_s, p_fl)
284 vfsgenerror (/*@sef@*/ flagSpec p_fs, /*@sef@*/ /*@only@*/ cstring p_s,
285 /*@sef@*/ fileloc p_loc)
286 /*@modifies *g_msgstream, internalState@*/ ;
287 #define vfsgenerror(fs, s, loc) ((void) fsgenerror(fs,s,loc))
290 ** Reports a warning when f1 is ON and f2 is ON
294 voptgenerror2 (/*@sef@*/ flagcode p_f1, /*@sef@*/ flagcode p_f2,
295 /*@sef@*/ /*@only@*/ cstring p_s, /*@sef@*/ fileloc p_loc);
296 #define voptgenerror2(f1, f2, s, loc) ((void) optgenerror2 (f1, f2, s, loc))
299 ** Reports a warning when f1 is ON and f2 is OFF
303 voptgenerror2n (/*@sef@*/ flagcode p_f1, /*@sef@*/ flagcode p_f2,
304 /*@sef@*/ /*@only@*/ cstring p_s, /*@sef@*/ fileloc p_loc);
305 #define voptgenerror2n(f1, f2, s, loc) ((void) optgenerror2n (f1, f2, s, loc))
307 extern void noptgenerror (/*@sef@*/ flagcode p_code,
308 /*@sef@*/ /*@only@*/ cstring p_s,
309 /*@sef@*/ fileloc p_loc);
310 /*@-branchstate@*/ /* sef only s is freed on one branch */
311 #define noptgenerror(o,s,loc) \
312 (context_suppressNotFlagMsg (o, loc) \
313 ? (flagcode_recordSuppressed(o), FALSE) \
314 : llnoptgenerror (o, s, loc))
318 vnoptgenerror (/*@sef@*/ flagcode p_code, /*@sef@*/ /*@only@*/ cstring p_msg,
319 /*@sef@*/ fileloc p_loc);
320 # define vnoptgenerror(o, s, loc) ((void) noptgenerror(o, s, loc))
323 vgenhinterror (flagcode p_code, /*@only@*/ cstring p_mst,
324 /*@only@*/ cstring p_hint, /*@sef@*/ fileloc p_loc);
325 # define vgenhinterror(o, s, h, loc) \
326 ((void) llgenhinterror(o, s, h, loc))
329 extern /*@private@*/ bool /*@alt void@*/ xllforceerror (char *p_srcFile, int p_srcLine, flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl)
330 /*@modifies g_msgstream@*/ ;
332 extern bool /*@alt void@*/ llforceerror (flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl)
333 /*@modifies g_msgstream@*/ ;
334 # define llforceerror(p_code, p_s, p_fl) \
335 (xllforceerror (__FILE__, __LINE__, p_code, p_s, p_fl))
337 extern /*@private@*/ bool xcppoptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
338 /*@only@*/ cstring p_s, cppReader *p_pfile)
339 /*@modifies g_msgstream, p_pfile@*/ ;
341 extern bool cppoptgenerror (flagcode p_code, /*@only@*/ cstring p_s, cppReader *p_pfile)
342 /*@modifies g_msgstream, p_pfile@*/ ;
343 # define cppoptgenerror(p_code, p_s, p_pfile) \
344 (xcppoptgenerror (__FILE__, __LINE__, p_code, p_s, p_pfile))
346 extern void llerrorlit (flagcode p_o, char *p_s);
347 # define llerrorlit(o, s) ((void) llerror (o, cstring_makeLiteral (s)))
349 extern void llgenindentmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_msgstream@*/ ;
351 extern /*@noreturn@*/ void llbugexitlit (char *p_s);
352 # define llbugexitlit(s) (llbug (cstring_makeLiteral (s)))
354 extern void llbuglit (char *p_s);
355 # define llbuglit(s) (llbug (cstring_makeLiteral (s)))
357 extern void llcontbuglit (char *p_s);
358 # define llcontbuglit(s) (llbug (cstring_makeLiteral (s)))
360 extern void checkParseError (void);
362 extern void llmsglit (char *p_s);
363 # define llmsglit(s) (llmsg (cstring_makeLiteral (s)))
365 extern void ppllerror (/*@only@*/ cstring p_s);
366 extern void genppllerrorhint (flagcode p_code, /*@only@*/ cstring p_s,
367 /*@only@*/ cstring p_hint);
368 extern void genppllerror (flagcode p_code, /*@only@*/ cstring p_s);
369 extern /*@unused@*/ void pplldiagmsg (/*@only@*/ cstring p_s);
370 extern void loadllmsg (/*@only@*/ cstring p_s);
372 extern void llgenindentmsgnoloc (/*@only@*/ cstring p_s);
374 extern /*@observer@*/ cstring lldecodeerror (int) /*@*/ ;
376 extern void prepareMessage (void) /*@modifies internalState, g_msgstream@*/ ;
377 extern void closeMessage (void) /*@modifies internalState, g_msgstream@*/ ;
379 extern void llflush (void) /*@modifies systemState@*/ ;
382 # error "Multiple include"