X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/146e25eb1ce61cf25ba20fd3db7b55fc6c74d3ad..27c9e6405d13abd5a1f1f0bae1ec7bb873abadea:/src/llmain.c

diff --git a/src/llmain.c b/src/llmain.c
index f3e8af0..1d9c6b5 100644
--- a/src/llmain.c
+++ b/src/llmain.c
@@ -1,6 +1,6 @@
 /*
 ** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Copyright (C) 1994-2002 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -787,7 +787,12 @@ int main (int argc, char *argv[])
 	    flagcode opt;
 
 	    thisarg++;
-	    opt = identifyFlag (cstring_fromChars (thisarg));
+
+	    /*
+	    ** Don't report warnings this time
+	    */
+
+	    opt = flags_identifyFlagQuiet (cstring_fromChars (thisarg));
 
 	    if (opt == FLG_NOF)
 	      {
@@ -1000,7 +1005,7 @@ int main (int argc, char *argv[])
 	      flagname = cstring_fromChars (thisarg);
 
 	      DPRINTF (("Flag: %s", flagname));
-	      opt = identifyFlag (flagname);
+	      opt = flags_identifyFlag (flagname);
 	      DPRINTF (("Flag: %s", flagcode_unparse (opt)));
 
 	      if (flagcode_isSkip (opt) || opt == FLG_SHOWSCAN || opt == FLG_WARNRC)
@@ -1532,7 +1537,7 @@ int main (int argc, char *argv[])
 	      }
 	    else
 	      {
-		specErrors = message ("%d spec warning%& found\n       ",
+		specErrors = message ("%d spec warning%&\n       ",
 				      nspecErrors);
 		expsuccess = FALSE;
 	      }
@@ -1579,7 +1584,7 @@ int main (int argc, char *argv[])
 		  if (!isQuiet)
 		    {
 		      llmsg (message ("Finished checking --- "
-				      "%s%d code warning%& found", 
+				      "%s%d code warning%&", 
 				      specErrors, context_numErrors ()));
 		    }
 
@@ -1794,7 +1799,7 @@ printParseErrors (void)
 	    "other compiler extensions by using a pre-processor define. "
 	    "Alternately, you can surround the unparseable code with");
   llmsglit ("");
-  llmsglit ("   # ifndef __LCLINT__");
+  llmsglit ("   # ifndef S_SPLINT_S");
   llmsglit ("   ...");
   llmsglit ("   # endif");
   llmsglit ("");
@@ -1931,11 +1936,11 @@ printAnnotations (void)
   llmsglit ("   /*@falsenull@*/ - if result is TRUE, first parameter is not NULL");
   llmsglit ("");
   llmsglit ("Execution:");
-  llmsglit ("   /*@exits@*/ - function never returns");
-  llmsglit ("   /*@mayexit@*/ - function may or may not return");
-  llmsglit ("   /*@trueexit@*/ - function does not return if first parameter is TRUE");
-  llmsglit ("   /*@falseexit@*/ - function does not return if first parameter if FALSE");
-  llmsglit ("   /*@neverexit@*/ - function always returns");
+  llmsglit ("   /*@noreturn@*/ - function never returns");
+  llmsglit ("   /*@maynotreturn@*/ - function may or may not return");
+  llmsglit ("   /*@noreturnwhentrue@*/ - function does not return if first parameter is TRUE");
+  llmsglit ("   /*@noreturnwhenfalse@*/ - function does not return if first parameter if FALSE");
+  llmsglit ("   /*@alwaysreturns@*/ - function always returns");
   llmsglit ("");
   llmsglit ("Side-Effects:");
   llmsglit ("   /*@sef@*/ - corresponding actual parameter has no side effects");
@@ -2218,7 +2223,7 @@ cleanupFiles (void)
 ** cleans up temp files (if necessary) and exits
 */
 
-/*@exits@*/ void
+/*@noreturn@*/ void
 llexit (int status)
 {
   DPRINTF (("llexit: %d", status));
@@ -2414,7 +2419,7 @@ loadrc (/*:open:*/ FILE *rcfile, cstringSList *passThroughArgs)
 
 	  DPRINTF (("Flag: %s", thisflag));
 
-	  opt = identifyFlag (cstring_fromChars (thisflag));
+	  opt = flags_identifyFlag (cstring_fromChars (thisflag));
 	  
 	  if (flagcode_isSkip (opt))
 	    {