Added manual test cases.

[splint.git] / src / llmain.c

diff --git a/src/llmain.c b/src/llmain.c
index f3e8af08a9f022656aa43c58f5bb59148f6f1f37..1d9c6b544f77ccde96134120b2a75cd7361058c2 100644 (file)
--- 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))
            {