Merged this branch with the one in the splint.sf.net repository.

[splint.git] / src / constraintTerm.c

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 868c9d551622252f1e82f7cac0020eefc82b9f06..08c840a99d0718519efd7cb97272d768e60d384d 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -37,13 +37,8 @@
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-/*@-czechfcns@*/
-/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
-/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
-/*@-nullpass@*/ /* !!! DRL needs to fix this code! */
-/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
-/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
+
 
 bool constraintTerm_isDefined (constraintTerm t)
 {
@@ -123,6 +118,7 @@ bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*
   return FALSE;
 }
 
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
 
 int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 {
@@ -151,7 +147,7 @@ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm
   return ret;  
 }
 
-
+/*@noaccess exprNode@*/
 
 bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
 {
@@ -581,10 +577,6 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
            fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
            cstring_free(ctString);
          }
-       else if (sRef_isField (s) )
-         {
-           fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) );
-         }
        else
          {
            u = sRef_getUentry(s);
@@ -634,6 +626,11 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
        sRef s;
        char * term;
        term = reader_getWord(&str);
+
+       if (term == NULL)
+         {
+           llfatalbug(message("Error reading internal library.  File may be currupted"));
+         }
        
        if (strcmp (term, "Result") == 0 )
          {
@@ -648,6 +645,11 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
 
            reader_checkChar(&str, ' ');
            str2  = reader_getWord(&str);
+           if (str2 ==  NULL)
+             {
+               llfatalbug(message("Error reading internal library.  File may be currupted"));
+             }
+           
            param = reader_getInt(&str);
 
            ostr2 = str2;
@@ -655,12 +657,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
            s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc));
            free (ostr2);
          }
-       else if (strcmp (term, "sRef_dump" ) == 0 )
-         {
-           reader_checkChar(&str, ' ');
-           s = sRef_undump (&str);
-         }
-       else  /* This must be an identified that we can search for in usymTab */
+       else  /* This must be an identifier that we can search for in usymTab */
          {
            cstring termStr = cstring_makeLiteralTemp(term);
 
@@ -681,6 +678,12 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
        cstring termStr;
                
        term = reader_getWord(&str);
+
+       if (term == NULL)
+         {
+           llfatalbug(message("Error reading internal library.  File may be currupted."));
+         }
+       
        /* This must be an identifier that we can search for in usymTab */
        termStr = cstring_makeLiteralTemp(term);
        
@@ -703,6 +706,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
       break;
       
     default:
+       llfatalbug(message("Error reading internal library.  File may be currupted."));
       BADEXIT;
     }
   free (os);