X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/b072092f32623dab70e6ffe1613740542ea66748..a9ec328054b628447830161535f4915f715f49cd:/src/Headers/llerror.h

diff --git a/src/Headers/llerror.h b/src/Headers/llerror.h
index 0090d29..eb76ba9 100644
--- a/src/Headers/llerror.h
+++ b/src/Headers/llerror.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
 ** See ../LICENSE for license information.
 **
 */
@@ -12,7 +12,7 @@ extern bool /*@alt void@*/ check (bool p_x);
 
 extern bool doCheck (bool p_x, cstring p_pred, cstring p_file, int p_line);
 
-extern /*@falseexit@*/ void llassert (/*@sef@*/ bool p_test);
+extern /*@noreturnwhenfalse@*/ void llassert (/*@sef@*/ bool p_test);
 /*@-macroredef@*/
 # define llassert(tst) \
     do { if (!(tst)) { \
@@ -23,14 +23,26 @@ extern /*@falseexit@*/ void llassert (/*@sef@*/ bool p_test);
        }} while (FALSE)
 /*@=macroredef@*/
 
-extern /*@falseexit@*/ void llassertretnull (/*@sef@*/ bool p_test);
+extern /*@noreturnwhenfalse@*/ void llassertretnull (/*@sef@*/ bool p_test);
 # define llassertretnull(tst) \
     do { if (!(tst)) { \
            if (context_getFlag (FLG_TRYTORECOVER)) checkParseError (); \
 	   lldiagmsg (message ("%s:%d: at source point", \
 			       cstring_makeLiteralTemp (__FILE__), __LINE__)); \
 	   llbuglit ("llassert failed: " #tst); \
-           return NULL; \
+       }} while (FALSE)
+
+typedef void *tx_voidptr;
+
+extern /*@noreturnwhenfalse@*/ void 
+llassertretval (/*@sef@*/ bool p_test, /*@sef@*/ /*@null@*/ tx_voidptr /*@alt anytype@*/ p_val); 
+# define llassertretval(tst,val) \
+    do { if (!(tst)) { \
+           if (context_getFlag (FLG_TRYTORECOVER)) checkParseError (); \
+	   lldiagmsg (message ("%s:%d: at source point", \
+			       cstring_makeLiteralTemp (__FILE__), __LINE__)); \
+	   llbuglit ("llassert failed: " #tst); \
+           /*@-type@*/ return (val); /*@=type@*/ \
        }} while (FALSE)
 
 /*
@@ -39,7 +51,7 @@ extern /*@falseexit@*/ void llassertretnull (/*@sef@*/ bool p_test);
 ** the normal error generation routines are used).
 */
 
-extern /*@falseexit@*/ void llassertprotect (/*@sef@*/ bool p_test);
+extern /*@noreturnwhenfalse@*/ void llassertprotect (/*@sef@*/ bool p_test);
 # define llassertprotect(tst) \
     do { if (!(tst)) { \
 	   fprintf (stderr, "%s:%d: at source point: ", __FILE__, __LINE__); \
@@ -47,7 +59,7 @@ extern /*@falseexit@*/ void llassertprotect (/*@sef@*/ bool p_test);
            llexit (EXIT_FAILURE); \
        }} while (FALSE)
 
-extern /*@falseexit@*/ void llassertfatal (/*@sef@*/ bool p_test);
+extern /*@noreturnwhenfalse@*/ void llassertfatal (/*@sef@*/ bool p_test);
 # define llassertfatal(tst) \
     do { if (!(tst)) \
 	   llfatalbug (message("%s:%d: fatal llassert failed: " #tst, \
@@ -55,79 +67,94 @@ extern /*@falseexit@*/ void llassertfatal (/*@sef@*/ bool p_test);
        } while (FALSE)
 
 /*
-** llassertprint and llassertprintret are in lclintMacros.nf
+** llassertprint and llassertprintret are in splintMacros.nf
 */
 
-extern void llmsg (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
+extern void llmsg (/*@only@*/ cstring p_s) /*@modifies g_warningstream@*/ ;
 
-extern void lldiagmsg (/*@only@*/ cstring p_s) /*@modifies stderr@*/ ;
-extern void llmsgplain (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
+extern void lldiagmsg (/*@only@*/ cstring p_s) /*@modifies g_messagestream@*/ ;
+extern void llmsgplain (/*@only@*/ cstring p_s) /*@modifies g_warningstream@*/ ;
 extern void llhint (/*@only@*/ cstring p_s) 
-   /*@globals g_currentloc, g_msgstream;@*/ 
-   /*@modifies g_msgstream@*/ ;
+   /*@globals g_currentloc, g_warningstream;@*/ 
+   /*@modifies g_warningstream@*/ ;
 
-extern /*@private@*/ /*@exits@*/ void xllfatalbug (char *p_srcFile, int p_srcLine,
-						  /*@only@*/ cstring p_s) 
+extern /*:private:*/ /*@noreturn@*/ void 
+xllfatalbug (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) 
    /*@globals g_currentloc@*/
-   /*@modifies stderr@*/ ;
+   /*@modifies g_errorstream@*/ ;
 
-extern /*@exits@*/ void llfatalbug (/*@only@*/ cstring p_s) 
+extern /*@noreturn@*/ void llfatalbug (/*@only@*/ cstring p_s) 
    /*@globals g_currentloc@*/
-   /*@modifies stderr@*/ ;
+   /*@modifies g_errorstream@*/ ;
+
 # define llfatalbug(p_s) \
      xllfatalbug (__FILE__, __LINE__, p_s)
 
-extern /*@private@*/ void xllgloberror (char *p_srcFile, int p_srcLine, 
-					/*@only@*/ cstring p_s)
-     /*@modifies g_msgstream@*/ ;
-
-extern void llgloberror (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
-# define llgloberror(p_s) \
-     xllgloberror (__FILE__, __LINE__, p_s)
-
-extern /*@private@*/ bool xllgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
+extern /*:private:*/ bool xllgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
 				       /*@only@*/ cstring p_s, fileloc p_fl)
-     /*@modifies g_msgstream@*/ ;
+     /*@modifies g_warningstream@*/ ;
 
 extern bool llgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_fl) 
-     /*@modifies g_msgstream@*/ ;
+     /*@modifies g_warningstream@*/ ;
 # define llgenerror(p_o, p_s, p_fl) \
      xllgenerror (__FILE__, __LINE__, p_o, p_s, p_fl)
 
-extern /*@private@*/ bool 
+extern /*:private:*/ bool 
    xllgenhinterror (char *p_srcFile, int p_srcLine,
 		    flagcode p_o, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint, 
 		    fileloc p_fl) 
-     /*@modifies g_msgstream@*/ ;
+     /*@modifies g_warningstream@*/ ;
 
 extern bool llgenhinterror (flagcode p_o, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint, 
-			    fileloc p_fl) /*@modifies g_msgstream@*/ ;
+			    fileloc p_fl) /*@modifies g_warningstream@*/ ;
 
 # define llgenhinterror(p_o, p_s, p_hint, p_fl) \
      xllgenhinterror (__FILE__, __LINE__, p_o, p_s, p_hint, p_fl)
 
 
 extern void llerror (flagcode p_o, /*@only@*/ cstring p_s) 
-   /*@globals g_msgstream, g_currentloc@*/ 
-   /*@modifies g_msgstream@*/ ;
+   /*@globals g_warningstream, g_currentloc@*/ 
+   /*@modifies g_warningstream@*/ ;
 # define llerror(p_o, p_s) \
    ((void) llgenerror (p_o, p_s, g_currentloc))
 
-extern void llgenmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_msgstream@*/ ;
-extern /*@exits@*/ void llfatalerror (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
-extern /*@exits@*/ void llfatalerrorLoc (/*@only@*/ cstring p_s) 
+extern void llgenmsg (/*@only@*/ cstring p_s, fileloc p_fl)
+   /*@modifies g_warningstream@*/ ;
+
+extern /*@noreturn@*/ /*:private:*/ 
+void xllfatalerror (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) 
+   /*@modifies g_errorstream@*/ ;
+
+extern /*@noreturn@*/ void llfatalerror (/*@only@*/ cstring p_s) 
+   /*@modifies g_errorstream@*/ ;
+# define llfatalerror(p_s) xllfatalerror (__FILE__, __LINE__, p_s)
+
+extern /*@noreturn@*/ /*:private:*/ void 
+xllfatalerrorLoc (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) 
+   /*@globals g_currentloc@*/ 
+   /*@modifies g_errorstream@*/ ;
+
+extern /*@noreturn@*/ void llfatalerrorLoc (/*@only@*/ cstring p_s) 
    /*@globals g_currentloc@*/ 
-   /*@modifies stderr@*/ ;
+   /*@modifies g_errorstream@*/ ;
+# define llfatalerrorLoc(p_s) xllfatalerrorLoc (__FILE__, __LINE__, p_s)
+
+extern /*:private:*/ void
+   xllparseerror (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s)
+   /*@globals g_currentloc@*/
+   /*@modifies g_warningstream@*/ ;
+
 extern void llparseerror (/*@only@*/ cstring p_s) 
-   /*@globals g_msgstream, g_currentloc@*/ 
-   /*@modifies g_msgstream@*/ ;
+   /*@globals g_currentloc@*/
+   /*@modifies g_warningstream@*/ ;
 
-# ifndef NOLCL
-extern /*@exits@*/ void lclplainfatalerror (/*@only@*/ cstring p_msg) /*@modifies g_msgstream@*/ ;
-extern /*@exits@*/ void lclfatalbug (/*@temp@*/ char *p_msg) /*@modifies g_msgstream@*/ ;
+# define llparseerror(p_s) xllparseerror (__FILE__, __LINE__, p_s)
+
+extern /*@noreturn@*/ void lclplainfatalerror (/*@only@*/ cstring p_msg) /*@modifies g_warningstream@*/ ;
+extern /*@noreturn@*/ void lclfatalbug (/*@temp@*/ char *p_msg) /*@modifies g_warningstream@*/ ;
 extern int lclNumberErrors (void) /*@*/ ;
 extern bool lclHadNewError (void) /*@modifies internalState@*/ ;
-extern /*@exits@*/ void lclfatalerror (ltoken p_t, /*@only@*/ cstring p_msg);
+extern /*@noreturn@*/ void lclfatalerror (ltoken p_t, /*@only@*/ cstring p_msg);
 
 extern void xlclerror (char *p_srcFile, int p_srcLine, ltoken p_t, /*@only@*/ cstring p_msg) ;
 
@@ -139,32 +166,43 @@ extern void lclbug (/*@only@*/ cstring p_s);
 extern void lclplainerror (/*@only@*/ cstring p_msg);
 extern bool lclHadError (void);
 extern void lclRedeclarationError (ltoken p_id);
-# endif
 
-extern void llerror_flagWarning (/*@only@*/ cstring p_s) /*@modifies g_msgstream@*/ ;
+extern void llerror_flagWarning (/*@only@*/ cstring p_s) /*@modifies g_warningstream@*/ ;
 
-extern /*@exits@*/ void llbugaux (cstring p_file, int p_line, /*@only@*/ cstring p_s) 
-   /*@globals g_msgstream, g_currentloc@*/
-   /*@modifies *g_msgstream@*/ ; 
+extern /*@noreturn@*/ void llbugaux (cstring p_file, int p_line, /*@only@*/ cstring p_s) 
+   /*@globals g_warningstream, g_currentloc@*/
+   /*@modifies *g_warningstream@*/ ; 
 
-extern /*@exits@*/ void llbug (/*@only@*/ cstring p_s) 
-   /*@globals g_msgstream, g_currentloc@*/
-   /*@modifies *g_msgstream@*/ ; 
+extern /*@noreturn@*/ void llbug (/*@only@*/ cstring p_s) 
+   /*@globals g_warningstream, g_currentloc@*/
+   /*@modifies *g_warningstream@*/ ; 
 
    /* doesn't really exit, but don't mind errors if it doesn't */
 # define llbug(s) llbugaux (cstring_makeLiteralTemp (__FILE__), __LINE__, s)
 
-extern void llquietbugaux (/*@only@*/ cstring p_s, cstring, int) /*@modifies *g_msgstream@*/ ; 
-extern void llquietbug (/*@only@*/ cstring) /*@modifies *g_msgstream@*/ ; 
+extern void llquietbugaux (/*@only@*/ cstring p_s, cstring, int) /*@modifies *g_warningstream@*/ ; 
+extern void llquietbug (/*@only@*/ cstring) /*@modifies *g_warningstream@*/ ; 
 # define llquietbug(s) llquietbugaux (s, cstring_makeLiteralTemp (__FILE__), __LINE__)
 
-extern void llcontbug (/*@only@*/ cstring p_s) /*@modifies *g_msgstream@*/ ; 
+extern void llcontbug (/*@only@*/ cstring p_s) /*@modifies *g_warningstream@*/ ; 
        /* doesn't really exit, but don't mind errors if it doesn't */
 # define llcontbug(s)  (llbug (s))
 
 extern void cleanupMessages (void) 
-   /*@globals g_msgstream, g_currentloc;@*/
-   /*@modifies g_msgstream, internalState@*/ ;
+   /*@globals g_warningstream, g_currentloc;@*/
+   /*@modifies g_warningstream, internalState@*/ ;
+
+extern void displayScan (/*@only@*/ cstring p_msg)
+  /*@modifies g_messagestream@*/ ;
+
+extern void displayScanOpen (/*@only@*/ cstring p_msg)
+  /*@modifies g_messagestream@*/ ;
+
+extern void displayScanContinue (/*@temp@*/ cstring p_msg)
+  /*@modifies g_messagestream@*/ ;
+
+extern void displayScanClose (void)
+  /*@modifies g_messagestream@*/ ;
 
 /*
 ** Report error iff f1 and f2 are set.
@@ -173,11 +211,11 @@ extern void cleanupMessages (void)
 extern bool 
 xoptgenerror2 (char *p_srcFile, int p_srcLine,
 	       flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool 
 optgenerror2 (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define optgenerror2(p_f1, p_f2, p_s, p_loc) \
   (xoptgenerror2 (__FILE__, __LINE__, p_f1, p_f2, p_s, p_loc))
 
@@ -188,42 +226,42 @@ optgenerror2 (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_lo
 extern bool 
 xoptgenerror2n (char *p_srcFile, int p_srcLine,
 		flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool 
 optgenerror2n (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define optgenerror2n(p_f1, p_f2, p_s, p_loc) \
   (xoptgenerror2n (__FILE__, __LINE__, p_f1, p_f2, p_s, p_loc))
 
-extern /*@private@*/ bool xlloptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+extern /*:private:*/ bool xlloptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool lloptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define lloptgenerror(p_o, p_s, p_loc) \
    (xlloptgenerror (__FILE__, __LINE__, p_o, p_s, p_loc))
 
 extern bool xllnoptgenerror (char *p_srcFile, int p_srcLine,
 			     flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool llnoptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define llnoptgenerror(p_o, p_s, p_loc) \
    (xllnoptgenerror (__FILE__, __LINE__, p_o, p_s, p_loc))
 
-extern /*@private@*/ bool 
+extern /*:private:*/ bool 
    xllgenformattypeerror (char *p_srcFile, int p_srcLine,
 			  ctype p_t1, exprNode p_e1, 
 			  ctype p_t2, exprNode p_e2,
 			  /*@only@*/ cstring p_s, fileloc p_fl)
-     /*@modifies *g_msgstream, internalState@*/ ;
+     /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool llgenformattypeerror (ctype p_t1, exprNode p_e1, 
 				  ctype p_t2, exprNode p_e2,
 				  /*@only@*/ cstring p_s, fileloc p_fl)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define llgenformattypeerror(p_t1, p_e1, p_t2, p_e2, p_s, p_fl) \
   xllgenformattypeerror (__FILE__, __LINE__, p_t1, p_e1, p_t2, p_e2, p_s, p_fl)
 
@@ -232,13 +270,13 @@ extern bool xllgentypeerror (char *p_srcFile, int p_srcLine,
 			     ctype p_t2, exprNode p_e2,
 			     /*@only@*/ cstring p_s,
 			     fileloc p_fl)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 extern bool llgentypeerror (ctype p_t1, exprNode p_e1,
 			    ctype p_t2, exprNode p_e2,
 			    /*@only@*/ cstring p_s,
 			    fileloc p_fl)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 # define llgentypeerror(p_t1, p_e1, p_t2, p_e2, p_s, p_fl) \
   xllgentypeerror (__FILE__, __LINE__, p_t1, p_e1, p_t2, p_e2, p_s, p_fl)
 
@@ -248,7 +286,7 @@ extern bool gentypeerror (/*@sef@*/ ctype p_t1,
 			  /*@sef@*/ exprNode p_e2,
 			  /*@sef@*/ /*@only@*/ cstring p_s,
 			  /*@sef@*/ fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 /*@-branchstate@*/ /* sef only s is freed on one branch */
 #define gentypeerror(t1, e1, t2, e2, s, loc)      \
@@ -265,7 +303,7 @@ extern bool gentypeerror (/*@sef@*/ ctype p_t1,
 extern bool 
   optgenerror (/*@sef@*/ flagcode p_o, /*@sef@*/ /*@only@*/ cstring p_s,
 	       /*@sef@*/ fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 
 /*@-branchstate@*/ /* sef only s is freed on one branch */
 #define optgenerror(o,s,loc)      \
@@ -276,23 +314,23 @@ extern bool
 extern void 
   voptgenerror (/*@sef@*/ flagcode p_o, /*@sef@*/ /*@only@*/ cstring p_s, 
 		/*@sef@*/ fileloc p_loc)
-  /*@modifies *g_msgstream, internalState@*/ ;
+  /*@modifies *g_warningstream, internalState@*/ ;
 #define voptgenerror(o, s, loc)   ((void) optgenerror(o,s,loc))
 
-extern /*@private@*/ bool 
+extern /*:private:*/ bool 
   xfsgenerror (char *p_srcFile, int p_srcLine,
 		flagSpec p_fs, /*@only@*/ cstring p_s, fileloc p_fl) 
-     /*@modifies g_msgstream, internalState@*/ ;
+     /*@modifies g_warningstream, internalState@*/ ;
 
 extern bool fsgenerror (flagSpec p_fs, /*@only@*/ cstring p_s, fileloc p_fl) 
-     /*@modifies g_msgstream, internalState@*/ ;
+     /*@modifies g_warningstream, internalState@*/ ;
 # define fsgenerror(p_fs, p_s, p_fl) \
      xfsgenerror (__FILE__, __LINE__, p_fs, p_s, p_fl)
 
 extern void 
 vfsgenerror (/*@sef@*/ flagSpec p_fs, /*@sef@*/ /*@only@*/ cstring p_s, 
 	     /*@sef@*/ fileloc p_loc)
-     /*@modifies *g_msgstream, internalState@*/ ;
+     /*@modifies *g_warningstream, internalState@*/ ;
 #define vfsgenerror(fs, s, loc)   ((void) fsgenerror(fs,s,loc))
 
 /*
@@ -335,29 +373,30 @@ extern void
     ((void) llgenhinterror(o, s, h, loc))
 
 
-extern /*@private@*/ bool /*@alt void@*/ xllforceerror (char *p_srcFile, int p_srcLine, flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) 
-     /*@modifies g_msgstream@*/ ; 
+extern /*:private:*/ bool /*@alt void@*/ xllforceerror (char *p_srcFile, int p_srcLine, flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) 
+     /*@modifies g_warningstream@*/ ; 
 
 extern bool /*@alt void@*/ llforceerror (flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) 
-     /*@modifies g_msgstream@*/ ; 
+     /*@modifies g_warningstream@*/ ; 
 # define llforceerror(p_code, p_s, p_fl) \
      (xllforceerror (__FILE__, __LINE__, p_code, p_s, p_fl))
 
-extern /*@private@*/ bool xcppoptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
+extern /*:private:*/ bool xcppoptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o,
 			     /*@only@*/ cstring p_s, cppReader *p_pfile)
-     /*@modifies g_msgstream, p_pfile@*/ ;
+     /*@modifies g_warningstream, p_pfile@*/ ;
 
-extern bool cppoptgenerror (flagcode p_code, /*@only@*/ cstring p_s, cppReader *p_pfile)
-     /*@modifies g_msgstream, p_pfile@*/ ;
+extern bool /*@alt void@*/
+cppoptgenerror (flagcode p_code, /*@only@*/ cstring p_s, cppReader *p_pfile)
+     /*@modifies g_warningstream, p_pfile@*/ ;
 # define cppoptgenerror(p_code, p_s, p_pfile) \
     (xcppoptgenerror (__FILE__, __LINE__, p_code, p_s, p_pfile))
 
 extern void llerrorlit (flagcode p_o, char *p_s);
 # define llerrorlit(o, s)   ((void) llerror (o, cstring_makeLiteral (s)))
 
-extern void llgenindentmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_msgstream@*/ ;
+extern void llgenindentmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_warningstream@*/ ;
 
-extern /*@exits@*/ void llbugexitlit (char *p_s);
+extern /*@noreturn@*/ void llbugexitlit (char *p_s);
 # define llbugexitlit(s)    (llbug (cstring_makeLiteral (s)))
 
 extern void llbuglit (char *p_s);
@@ -372,6 +411,7 @@ extern void llmsglit (char *p_s);
 # define llmsglit(s)        (llmsg (cstring_makeLiteral (s)))
 
 extern void ppllerror (/*@only@*/ cstring p_s);
+
 extern void genppllerrorhint (flagcode p_code, /*@only@*/ cstring p_s, 
 			      /*@only@*/ cstring p_hint);
 extern void genppllerror (flagcode p_code, /*@only@*/ cstring p_s);
@@ -382,8 +422,15 @@ extern void llgenindentmsgnoloc (/*@only@*/ cstring p_s);
 
 extern /*@observer@*/ cstring lldecodeerror (int) /*@*/ ;
 
-extern void prepareMessage (void) /*@modifies internalState, g_msgstream@*/ ;
-extern void closeMessage (void) /*@modifies internalState, g_msgstream@*/ ;
+/*
+** should be static, but used in cpperror (which shouldn't exist)
+*/
+
+extern void prepareMessage (void)
+  /*@modifies internalState, g_messagestream@*/ ;
+
+extern void closeMessage (void)
+  /*@modifies internalState, g_messagestream@*/ ;
 
 extern void llflush (void) /*@modifies systemState@*/ ;