Fixed some /@*i@*/ comments in the code.

[splint.git] / src / cstring.c

diff --git a/src/cstring.c b/src/cstring.c
index 256954600e011206cdf00e016a25cd10a1fbc096..4c9f2c05cd548aa6679f82e8c0b81348b573d606 100644 (file)
--- a/src/cstring.c
+++ b/src/cstring.c
@@ -1,6 +1,6 @@
 /*
 ** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -50,9 +50,9 @@ char cstring_firstChar (cstring s)
   return (s[0]);
 }
 
-char cstring_getChar (cstring s, int n) 
+char cstring_getChar (cstring s, size_t n) 
 {
-  int length = cstring_length (s);
+  size_t length = cstring_length (s);
 
   llassert (cstring_isDefined (s));
   llassert (n >= 1 && n <= length);
@@ -60,7 +60,7 @@ char cstring_getChar (cstring s, int n)
   return (s[n - 1]);
 }
 
-cstring cstring_suffix (cstring s, int n) 
+cstring cstring_suffix (cstring s, size_t n) 
 {
   llassert (cstring_isDefined (s));
   llassert (n <= cstring_length (s));
@@ -68,7 +68,9 @@ cstring cstring_suffix (cstring s, int n)
   return (s + n);
 }
 
-cstring cstring_prefix (cstring s, int n) /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/ /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
+cstring cstring_prefix (cstring s, size_t n) 
+   /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/
+   /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
 {
   cstring t;
   char c;
@@ -137,7 +139,7 @@ cstring cstring_beforeChar (cstring s, char c)
   return cstring_undefined;
 }
 
-void cstring_setChar (cstring s, int n, char c) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
+void cstring_setChar (cstring s, size_t n, char c) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
 {
   llassert (cstring_isDefined (s));
   llassert (n > 0 && n <= cstring_length (s));
@@ -147,7 +149,7 @@ void cstring_setChar (cstring s, int n, char c) /*@requires maxRead(s) >= (n - 1
 
 char cstring_lastChar (cstring s) 
 {
-  int length;
+  size_t length;
 
   llassert (cstring_isDefined (s));
 
@@ -169,11 +171,11 @@ char cstring_lastChar (cstring s)
     }
 }
 
-/*@only@*/ cstring cstring_copyLength (char *s, int len) /*@requires maxSet(s) >= (len - 1) @*/
+/*@only@*/ cstring cstring_copyLength (char *s, size_t len) /*@requires maxSet(s) >= (len - 1) @*/
 {
   char *res = mstring_create (len + 1);
 
-  strncpy (res, s, size_fromInt (len));
+  strncpy (res, s, len);
   res[len] = '\0';
   return res;
 }
@@ -259,11 +261,12 @@ void cstring_stripChars (cstring s, const char *clist)
   if (cstring_isDefined (s))
     {
       int i;
-      int size = cstring_length (s);
+      size_t size = cstring_length (s);
 
-      for (i = 0; i < size; i++)
+      for (i = 0; i < size_toInt (size); i++)
        {
-/*drl bee: is*/          char c = s[i];
+               
+         char c = s[i];
          
          if (strchr (clist, c) != NULL)
            {
@@ -271,13 +274,13 @@ void cstring_stripChars (cstring s, const char *clist)
              int j;
              
              size--;
-
-             for (j = i; j < size; j++)
+             
+             for (j = i; j < size_toInt (size); j++)
                {
-       /*drl bee: is*/         /*drl bee: is*/   s[j] = s[j+1];
+                 s[j] = s[j+1];
                }
-
-         /*drl bee: is*/     s[size] = '\0'; 
+             
+             s[size] = '\0'; 
              i--;
            }
        }
@@ -323,9 +326,10 @@ static char lookLike (char c) /*@*/
 }
 
 cmpcode cstring_genericEqual (cstring s, cstring t,
-                             int nchars,
+                             size_t nchars,
                              bool caseinsensitive,
-                             bool lookalike)  /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
+                             bool lookalike) 
+  /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
 {
   if (s == t) return CGE_SAME;
   else if (cstring_isUndefined (s))
@@ -344,7 +348,7 @@ cmpcode cstring_genericEqual (cstring s, cstring t,
 
       while (*s != '\0')
        {
-         if (nchars > 0 && i >= nchars)
+         if (nchars > 0 && i >= size_toInt (nchars))
            {
              break;
            }
@@ -371,8 +375,7 @@ cmpcode cstring_genericEqual (cstring s, cstring t,
          t++;
        }
 
-  /*drl bee: ib*/
-      /*drl bee: ib*/ 
+        
       if (*s == '\0' && *t != '\0')
        {
          return CGE_DISTINCT;
@@ -411,12 +414,12 @@ bool cstring_equal (cstring c1, cstring c2)
   else return (strcmp (c1, c2) == 0);
 }
 
-bool cstring_equalLen (cstring c1, cstring c2, int len)
+bool cstring_equalLen (cstring c1, cstring c2, size_t len)
 {
   if (c1 == c2) return TRUE;
   else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
   else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
-  else return (strncmp (c1, c2, size_fromInt (len)) == 0);
+  else return (strncmp (c1, c2, len) == 0);
 }
 
 bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
@@ -427,10 +430,8 @@ bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
   else return (cstring_genericEqual (c1, c2, 0, TRUE, FALSE) != CGE_DISTINCT);
 }
 
-bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
+bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, size_t len)
 {
-  llassert (len >= 0);
-
   if (c1 == c2) return TRUE;
   else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
   else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
@@ -544,12 +545,13 @@ cstring cstring_fromChars (/*@exposed@*/ const char *cp)
     }
 }
 
-int cstring_length (cstring s)
+size_t cstring_length (cstring s)
 {
   if (cstring_isDefined (s))
     {
-      return size_toInt (strlen (s));
+      return strlen (s);
     }
+
   return 0;
 }
 
@@ -580,7 +582,7 @@ cstring_capitalizeFree (cstring s) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0
 }
 
 cstring
-cstring_clip (cstring s, int len)
+cstring_clip (cstring s, size_t len)
 {
   if (cstring_isUndefined (s) || cstring_length (s) <= len)
     {
@@ -589,14 +591,15 @@ cstring_clip (cstring s, int len)
   else
     {
       llassert (s != NULL);
-    /*drl bee: mrms*/   *(s + len) = '\0';
+      
+      *(s + len) = '\0';
     }
-
+  
   return s;
 }
 
 /*@only@*/ cstring
-cstring_elide (cstring s, int len)
+cstring_elide (cstring s, size_t len)
 {
   if (cstring_isUndefined (s) || cstring_length (s) <= len)
     {
@@ -605,30 +608,31 @@ cstring_elide (cstring s, int len)
   else
     {
       cstring sc = cstring_create (len);
-     
-      strncpy (sc, s, size_fromInt (len));
-     /*drl bee: mrms*/  *(sc + len - 1) = '\0';
+      
+      strncpy (sc, s, len);
+      
+      *(sc + len - 1) = '\0';
       *(sc + len - 2) = '.';      
       *(sc + len - 3) = '.';      
       *(sc + len - 4) = '.';      
+      
       return sc;
     }
 }
 
 /*@only@*/ cstring
-cstring_fill (cstring s, int n) /*@requires n >= 0 @*/
+cstring_fill (cstring s, size_t n) /*@requires n >= 0 @*/
 {
   cstring t = cstring_create (n + 1);
   cstring ot = t;
-  int len = cstring_length (s);
-  int i;
+  size_t len = cstring_length (s);
+  size_t i;
   
   if (len > n)
     {
       for (i = 0; i < n; i++)
        {
-       /*drl bee: is*/
-         /*drl bee: is*/ 
+                 
          *t++ = *s++;
        }
       *t = '\0';
@@ -637,13 +641,12 @@ cstring_fill (cstring s, int n) /*@requires n >= 0 @*/
     {
       for (i = 0; i < len; i++)
        {
-       /*drl bee: is*/
-/*drl bee: is*/ 
+       
          *t++ = *s++;
        }
       for (i = 0; i < n - len; i++)
        {
-/*drl bee: is*/ 
+
          *t++ = ' ';
        }
       *t = '\0';
@@ -661,7 +664,7 @@ cstring_downcase (cstring s)
       cstring ot = t;
       char c;
       
- /*drl bee: lhnt*/      while ((c = *s) != '\0')
+      while ((c = *s) != '\0')
        {
          if (c >= 'A' && c <= 'Z')
            {
@@ -670,7 +673,7 @@ cstring_downcase (cstring s)
          *t++ = c;
          s++;
        }
-     /*drl bee: is*/  *t = '\0';
+      *t = '\0';
       
       return ot;
     }
@@ -683,7 +686,7 @@ cstring_downcase (cstring s)
 /*@notnull@*/ cstring 
 cstring_appendChar (/*@only@*/ cstring s1, char c)
 {
-  int l = cstring_length (s1);
+  size_t l = cstring_length (s1);
   char *s;
 
   s = (char *) dmalloc (sizeof (*s) * (l + 2));
@@ -692,13 +695,13 @@ cstring_appendChar (/*@only@*/ cstring s1, char c)
     {  
       strcpy (s, s1);
       *(s + l) = c;
-      /*drl bee: dm*/ *(s + l + 1) = '\0';
+      *(s + l + 1) = '\0';
       sfree (s1); 
     }
   else
     {
       *(s) = c;
-      /*drl bee: dm*/  *(s + 1) = '\0';
+       *(s + 1) = '\0';
     } 
 
   return s;
@@ -721,7 +724,6 @@ cstring_concatFree1 (cstring s, cstring t)
   return res;
 }
 
-# ifndef NOLCL
 /*@only@*/ cstring 
 cstring_concatChars (cstring s, char *t)
 {
@@ -729,10 +731,9 @@ cstring_concatChars (cstring s, char *t)
   cstring_free (s);
   return res;
 }
-# endif
 
 /*@only@*/ cstring 
-cstring_concatLength (cstring s1, char *s2, int len) /*@requires maxSet(s2) >= (len - 1) @*/
+cstring_concatLength (cstring s1, char *s2, size_t len) /*@requires maxSet(s2) >= (len - 1) @*/
 {
   cstring tmp = cstring_copyLength (s2, len);
   cstring res = cstring_concat (s1, tmp);
@@ -749,7 +750,7 @@ cstring_concat (cstring s, cstring t) /*@requires maxSet(s) >= 0 @*/
 
   if (cstring_isDefined (s))
     {
-    /*drl bee: sl*/   strcpy (ret, s);
+      strcpy (ret, s);
     }
   if (cstring_isDefined (t))
     {
@@ -771,10 +772,10 @@ cstring_prependCharO (char c, /*@only@*/ cstring s1)
 /*@notnull@*/ /*@only@*/ cstring 
 cstring_prependChar (char c, /*@temp@*/ cstring s1)
 {
-  int l = cstring_length (s1);
+  size_t l = cstring_length (s1);
   char *s = (char *) dmalloc (sizeof (*s) * (l + 2));
   
-/*drl bee: dm*/   *(s) = c;
+  *(s) = c;
 
   if (cstring_isDefined (s1)) 
     {
@@ -783,11 +784,10 @@ cstring_prependChar (char c, /*@temp@*/ cstring s1)
       /*@=mayaliasunique@*/ 
     }
 
- /*drl bee: dm*/ *(s + l + 1) = '\0';
+ *(s + l + 1) = '\0';
   return s;
 }
 
-# ifndef NOLCL
 bool
 cstring_hasNonAlphaNumBar (cstring s)
 {
@@ -795,7 +795,7 @@ cstring_hasNonAlphaNumBar (cstring s)
 
   if (cstring_isUndefined (s)) return FALSE;
 
-/*drl bee: lhnt*/  while ((c = (int) *s) != (int) '\0')
+ while ((c = (int) *s) != (int) '\0')
     {
       if ((isalnum (c) == 0) && (c != (int) '_')
          && (c != (int) '.') && (c != (int) CONNECTCHAR))
@@ -807,30 +807,28 @@ cstring_hasNonAlphaNumBar (cstring s)
     }
   return FALSE;
 }
-# endif
 
 /*@only@*/ /*@notnull@*/ cstring 
-cstring_create (int n)
+cstring_create (size_t n)
 {
   char *s = dmalloc (sizeof (*s) * (n + 1));
-
- /*drl bee: dm*/ *s = '\0';
+  
+  *s = '\0';
   return s;
 }
 
 /*@only@*/ /*@notnull@*/ cstring
-cstring_copySegment (cstring s, int findex, int tindex)
+cstring_copySegment (cstring s, size_t findex, size_t tindex)
 {
   cstring res = cstring_create (tindex - findex + 1);
 
   llassert (cstring_isDefined (s));
   llassert (cstring_length (s) > tindex);
 
-  strncpy (res, (s + findex), size_fromInt ((tindex - findex + 1)));
+  strncpy (res, (s + findex), size_fromInt (size_toInt (tindex - findex) + 1));
   return res;
 }
 
-# ifndef NOLCL
 lsymbol cstring_toSymbol (cstring s)
 {
   lsymbol res = lsymbol_fromString (s);
@@ -838,7 +836,6 @@ lsymbol cstring_toSymbol (cstring s)
   cstring_free (s);
   return res;
 }
-# endif
 
 cstring cstring_bsearch (cstring key, char **table, int nentries)
 {
@@ -880,7 +877,7 @@ cstring cstring_bsearch (cstring key, char **table, int nentries)
       if (mid != 0 && mid < nentries - 1)
        {
          llassert (cstring_compare (key, table[mid - 1]) > 0);
-       /*drl bee: ndv*/  llassert (cstring_compare (key, table[mid + 1]) < 0);
+        llassert (cstring_compare (key, table[mid + 1]) < 0);
        }
 
       return res;
@@ -894,7 +891,7 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
   if (cstring_isDefined (s)) {
     char *t = s;
 
- /*drl bee: lhnt*/   while (*t != '\0' && isspace ((int) *t)) {
+   while (*t != '\0' && isspace ((int) *t)) {
       t++;
     }
 
@@ -976,16 +973,15 @@ static mstring doMergeString (cstring s)
   return ret;
 }
 
-static mstring doExpandEscapes (cstring s, /*@out@*/ int * len)
+static mstring doExpandEscapes (cstring s, /*@out@*/ size_t *len)
 {
   char *ptr;
   mstring ret;
   char * retPtr;
-
   
   llassert(cstring_isDefined (s));
   
-  ret = mstring_create (cstring_length(s) );
+  ret = mstring_create (cstring_length(s));
 
   ptr = s;
 
@@ -1123,23 +1119,20 @@ static mstring doExpandEscapes (cstring s, /*@out@*/ int * len)
 /*this function is like sctring_expandEscapses */
 mstring cstring_expandEscapes (cstring s)
 {
-  int len;
+  size_t len;
 
   mstring ret;
-  
   ret = doExpandEscapes (s, &len);
   return ret;
 }
 
-int  cstring_lengthExpandEscapes (cstring s)
+size_t cstring_lengthExpandEscapes (cstring s)
 {
-  int len;
-
+  size_t len;
   mstring tmpStr, tmpStr2;
 
   tmpStr = doMergeString (s);
   tmpStr2 = doExpandEscapes (tmpStr, &len);
-
   
   cstring_free(tmpStr);
   cstring_free(tmpStr2);
@@ -1147,8 +1140,6 @@ int  cstring_lengthExpandEscapes (cstring s)
   return len;
 }
 
-
-
 cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar)
 {
   char *ptr;
@@ -1169,3 +1160,11 @@ cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar
 
   return c;
 }
+
+
+
+
+
+
+
+