X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/616915ddfdcba888735f45cbd9c26c9b5383ee2c..1810fe2ad9d1641fb15f1374c5a44c166b22f97b:/src/cstring.c

diff --git a/src/cstring.c b/src/cstring.c
index 7352a00..8c877b2 100644
--- a/src/cstring.c
+++ b/src/cstring.c
@@ -1,6 +1,6 @@
 /*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -17,9 +17,9 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
 */
 /*
 ** cstring.c
@@ -31,12 +31,12 @@
  * - cstring_replaceAll () needed in cpplib.c
  */
 
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "osd.h"
 # include "portab.h"
 
-static /*@only@*/ /*@notnull@*/ 
+/*@only@*/ /*@notnull@*/ 
 cstring cstring_newEmpty (void)
 {
   return (cstring_create (0));
@@ -68,7 +68,7 @@ cstring cstring_suffix (cstring s, int n)
   return (s + n);
 }
 
-cstring cstring_prefix (cstring s, int n) 
+cstring cstring_prefix (cstring s, int n) /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/ /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
 {
   cstring t;
   char c;
@@ -108,6 +108,12 @@ int cstring_toPosInt (cstring s)
   return val;
 }
 
+cstring cstring_afterChar (cstring s, char c) 
+{
+  llassert (cstring_isDefined (s));
+  return strchr (s, c);
+}
+
 cstring cstring_beforeChar (cstring s, char c)
 {
   if (cstring_isDefined (s))
@@ -131,7 +137,7 @@ cstring cstring_beforeChar (cstring s, char c)
   return cstring_undefined;
 }
 
-void cstring_setChar (cstring s, int n, char c) 
+void cstring_setChar (cstring s, int n, char c) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
 {
   llassert (cstring_isDefined (s));
   llassert (n > 0 && n <= cstring_length (s));
@@ -151,7 +157,7 @@ char cstring_lastChar (cstring s)
   return (s[length - 1]);
 }
 
-/*@only@*/ cstring cstring_copy (cstring s) 
+/*@only@*/ cstring cstring_copy (cstring s) /*@ensures maxSet(result) == maxRead(s) /\ maxRead(result) == maxRead(s) @*/
 {
   if (cstring_isDefined (s))
     {
@@ -163,7 +169,7 @@ char cstring_lastChar (cstring s)
     }
 }
 
-/*@only@*/ cstring cstring_copyLength (char *s, int len)
+/*@only@*/ cstring cstring_copyLength (char *s, int len) /*@requires maxSet(s) >= (len - 1) @*/
 {
   char *res = mstring_create (len + 1);
 
@@ -188,7 +194,6 @@ bool cstring_containsChar (cstring c, char ch)
 ** Replaces all occurances of old in s with new.
 */
 
-# if defined (WIN32) || defined (OS2)
 void cstring_replaceAll (cstring s, char old, char snew)
 {
   
@@ -206,13 +211,12 @@ void cstring_replaceAll (cstring s, char old, char snew)
 
           }
 }
-# endif
 
-void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew)
+void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) 
+   /*@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @*/
 {
-  
   llassert (strlen (old) >= strlen (snew));
-
+  
   if (cstring_isDefined (s))
     {
       char *sp = strstr (s, old);
@@ -221,12 +225,15 @@ void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew)
 	{
 	  int lendiff = size_toInt (strlen (old) - strlen (snew));
 	  char *tsnew = snew;
-	  
+
+	  llassert (lendiff >= 0);
+
 	  while (*tsnew != '\0')
 	    {
+	      llassert (*sp != '\0');
 	      *sp++ = *tsnew++;
 	    }
-
+	  
 	  if (lendiff > 0)
 	    {
 	      while (*(sp + lendiff) != '\0')
@@ -234,13 +241,13 @@ void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew)
 		  *sp = *(sp + lendiff);
 		  sp++;
 		}
-
+	      
 	      *sp = '\0';
 	    }
 
 	  sp = strstr (s, old);
 	}
-          }
+    }
 }
 
 /*
@@ -256,7 +263,7 @@ void cstring_stripChars (cstring s, const char *clist)
 
       for (i = 0; i < size; i++)
 	{
-	  char c = s[i];
+/*drl bee: is*/ 	  char c = s[i];
 	  
 	  if (strchr (clist, c) != NULL)
 	    {
@@ -267,10 +274,10 @@ void cstring_stripChars (cstring s, const char *clist)
 
 	      for (j = i; j < size; j++)
 		{
-		  s[j] = s[j+1];
+	/*drl bee: is*/ 	/*drl bee: is*/   s[j] = s[j+1];
 		}
 
-	      s[size] = '\0'; 
+	  /*drl bee: is*/     s[size] = '\0'; 
 	      i--;
 	    }
 	}
@@ -318,7 +325,7 @@ static char lookLike (char c) /*@*/
 cmpcode cstring_genericEqual (cstring s, cstring t,
 			      int nchars,
 			      bool caseinsensitive,
-			      bool lookalike)
+			      bool lookalike)  /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
 {
   if (s == t) return CGE_SAME;
   else if (cstring_isUndefined (s))
@@ -364,6 +371,8 @@ cmpcode cstring_genericEqual (cstring s, cstring t,
 	  t++;
 	}
 
+  /*drl bee: ib*/
+      /*drl bee: ib*/ 
       if (*s == '\0' && *t != '\0')
 	{
 	  return CGE_DISTINCT;
@@ -428,7 +437,7 @@ bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
   else return (cstring_genericEqual (c1, c2, len, TRUE, FALSE) != CGE_DISTINCT);
 }
 
-bool cstring_equalPrefix (cstring c1, char *c2)
+bool cstring_equalPrefix (cstring c1, cstring c2)
 {
   llassert (c2 != NULL);
 
@@ -440,7 +449,7 @@ bool cstring_equalPrefix (cstring c1, char *c2)
   return (strncmp (c1, c2, strlen (c2)) == 0);
 }
 
-bool cstring_equalCanonicalPrefix (cstring c1, char *c2)
+bool cstring_equalPrefixLit (cstring c1, const char *c2)
 {
   llassert (c2 != NULL);
 
@@ -449,78 +458,7 @@ bool cstring_equalCanonicalPrefix (cstring c1, char *c2)
       return (strlen (c2) == 0);
     }
 
-# if defined (WIN32) || defined (OS2)
-  /*
-  ** If one has a drive specification, but the other doesn't, skip it.
-  */
-  
-  if (strchr (c1, ':') == NULL
-      && strchr (c2, ':') != NULL)
-    {
-      c2 = strchr (c2 + 1, ':');
-    }
-  else 
-    {
-      if (strchr (c2, ':') == NULL
-	  && strchr (c1, ':') != NULL)
-	{
-	  c1 = strchr (c1 + 1, ':');
-	}
-    }
-
-  {
-    int len = size_toInt (strlen (c2));
-    int i = 0;
-    int slen = 0;
-
-    if (cstring_length (c1) < len)
-      {
-	return FALSE;
-      }
-
-    for (i = 0; i < len; i++)
-      {
-	if (c1[slen] == c2[i]
-	    || (osd_isConnectChar (c1[slen]) && osd_isConnectChar (c2[i])))
-	  {
-	    ;
-	  }
-	else 
-	  {
-	    /*
-	    ** We allow \\ to match \ because MS-DOS screws up the directory
-	    ** names.
-	    */
-	    
-	    if (c1[slen] == '\\'
-		&& (slen > 0
-		    && c1[slen - 1] == '\\'
-		    && c2[i - 1] == '\\'))
-	      {
-		slen++;
-		if (c1[slen] != c2[i])
-		  {
-		    return FALSE;
-		  }
-	      }
-	    else
-	      {
-		return FALSE;
-	      }
-	  }
-
-	slen++;
-	if (slen >= cstring_length (c1))
-	  {
-	    return FALSE;
-	  }
-      }
-  }
-
-  return TRUE;
-# else
   return (strncmp (c1, c2, strlen (c2)) == 0);
-# endif
 }
 
 int cstring_xcompare (cstring *c1, cstring *c2)
@@ -613,7 +551,7 @@ int cstring_length (cstring s)
 }
 
 cstring
-cstring_capitalize (cstring s)
+cstring_capitalize (cstring s) /*@requires maxSet(s) >= 0 @*/
 {
   if (!cstring_isEmpty (s))
     {
@@ -627,7 +565,7 @@ cstring_capitalize (cstring s)
 }
 
 cstring
-cstring_capitalizeFree (cstring s)
+cstring_capitalizeFree (cstring s) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @*/
 {
   if (!cstring_isEmpty (s))
     {
@@ -648,7 +586,7 @@ cstring_clip (cstring s, int len)
   else
     {
       llassert (s != NULL);
-      *(s + len) = '\0';
+    /*drl bee: mrms*/   *(s + len) = '\0';
     }
 
   return s;
@@ -666,7 +604,7 @@ cstring_elide (cstring s, int len)
       cstring sc = cstring_create (len);
      
       strncpy (sc, s, size_fromInt (len));
-      *(sc + len - 1) = '\0';
+     /*drl bee: mrms*/  *(sc + len - 1) = '\0';
       *(sc + len - 2) = '.';      
       *(sc + len - 3) = '.';      
       *(sc + len - 4) = '.';      
@@ -675,7 +613,7 @@ cstring_elide (cstring s, int len)
 }
 
 /*@only@*/ cstring
-cstring_fill (cstring s, int n)
+cstring_fill (cstring s, int n) /*@requires n >= 0 @*/
 {
   cstring t = cstring_create (n + 1);
   cstring ot = t;
@@ -686,6 +624,8 @@ cstring_fill (cstring s, int n)
     {
       for (i = 0; i < n; i++)
 	{
+	/*drl bee: is*/
+	  /*drl bee: is*/ 
 	  *t++ = *s++;
 	}
       *t = '\0';
@@ -694,10 +634,13 @@ cstring_fill (cstring s, int n)
     {
       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';
@@ -715,7 +658,7 @@ cstring_downcase (cstring s)
       cstring ot = t;
       char c;
       
-      while ((c = *s) != '\0')
+ /*drl bee: lhnt*/      while ((c = *s) != '\0')
 	{
 	  if (c >= 'A' && c <= 'Z')
 	    {
@@ -724,7 +667,7 @@ cstring_downcase (cstring s)
 	  *t++ = c;
 	  s++;
 	}
-      *t = '\0';
+     /*drl bee: is*/  *t = '\0';
       
       return ot;
     }
@@ -746,13 +689,13 @@ cstring_appendChar (/*@only@*/ cstring s1, char c)
     {  
       strcpy (s, s1);
       *(s + l) = c;
-      *(s + l + 1) = '\0';
+      /*drl bee: dm*/ *(s + l + 1) = '\0';
       sfree (s1); 
     }
   else
     {
       *(s) = c;
-      *(s + 1) = '\0';
+      /*drl bee: dm*/  *(s + 1) = '\0';
     } 
 
   return s;
@@ -786,7 +729,7 @@ cstring_concatChars (cstring s, char *t)
 # endif
 
 /*@only@*/ cstring 
-cstring_concatLength (cstring s1, char *s2, int len)
+cstring_concatLength (cstring s1, char *s2, int len) /*@requires maxSet(s2) >= (len - 1) @*/
 {
   cstring tmp = cstring_copyLength (s2, len);
   cstring res = cstring_concat (s1, tmp);
@@ -797,13 +740,13 @@ cstring_concatLength (cstring s1, char *s2, int len)
 }
 
 /*@only@*/ cstring 
-cstring_concat (cstring s, cstring t)
+cstring_concat (cstring s, cstring t) /*@requires maxSet(s) >= 0 @*/
 {
   char *ret = mstring_create (cstring_length (s) + cstring_length (t));
 
   if (cstring_isDefined (s))
     {
-      strcpy (ret, s);
+    /*drl bee: sl*/   strcpy (ret, s);
     }
   if (cstring_isDefined (t))
     {
@@ -828,7 +771,7 @@ cstring_prependChar (char c, /*@temp@*/ cstring s1)
   int l = cstring_length (s1);
   char *s = (char *) dmalloc (sizeof (*s) * (l + 2));
   
-  *(s) = c;
+/*drl bee: dm*/   *(s) = c;
 
   if (cstring_isDefined (s1)) 
     {
@@ -837,7 +780,7 @@ cstring_prependChar (char c, /*@temp@*/ cstring s1)
       /*@=mayaliasunique@*/ 
     }
 
-  *(s + l + 1) = '\0';
+ /*drl bee: dm*/ *(s + l + 1) = '\0';
   return s;
 }
 
@@ -849,7 +792,7 @@ cstring_hasNonAlphaNumBar (cstring s)
 
   if (cstring_isUndefined (s)) return FALSE;
 
-  while ((c = (int) *s) != (int) '\0')
+/*drl bee: lhnt*/  while ((c = (int) *s) != (int) '\0')
     {
       if ((isalnum (c) == 0) && (c != (int) '_')
 	  && (c != (int) '.') && (c != (int) CONNECTCHAR))
@@ -868,14 +811,26 @@ cstring_create (int n)
 {
   char *s = dmalloc (sizeof (*s) * (n + 1));
 
-  *s = '\0';
+ /*drl bee: dm*/ *s = '\0';
   return s;
 }
 
+/*@only@*/ /*@notnull@*/ cstring
+cstring_copySegment (cstring s, int findex, int 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)));
+  return res;
+}
+
 # ifndef NOLCL
 lsymbol cstring_toSymbol (cstring s)
 {
-  lsymbol res = lsymbol_fromChars (cstring_toCharsSafe (s));
+  lsymbol res = lsymbol_fromString (s);
 
   cstring_free (s);
   return res;
@@ -922,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);
-	  llassert (cstring_compare (key, table[mid + 1]) < 0);
+	/*drl bee: ndv*/  llassert (cstring_compare (key, table[mid + 1]) < 0);
 	}
 
       return res;
@@ -936,7 +891,7 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
   if (cstring_isDefined (s)) {
     char *t = s;
 
-    while (*t != '\0' && isspace ((int) *t)) {
+ /*drl bee: lhnt*/   while (*t != '\0' && isspace ((int) *t)) {
       t++;
     }
 
@@ -945,6 +900,174 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
   
   return cstring_undefined;
 }
-    
+
+static mstring doExpandEscapes (cstring s, /*@out@*/ int * len)
+{
+  char *ptr;
+  mstring ret;
+  char * retPtr;
+
+  
+  llassert(cstring_isDefined (s));
+  
+  ret = mstring_create (cstring_length(s) );
+
+  ptr = s;
+
+  retPtr = ret;
+  while (*ptr != '\0')
+    {
+      if (*ptr != '\\')
+	{
+	  *retPtr = *ptr;
+	  retPtr++;
+	  ptr++;
+	  continue;
+	}
+      
+      if (*ptr == '\\')
+	{
+	  ptr++;
+	  if (*ptr == '\0')
+	    {
+	      /*not a legal escape sequence but try to handle it in a sesible way*/
+	      *retPtr = '\\';
+	      retPtr++;
+	    }
+	  
+	  // Handle Octal escapes 
+	  else if (*ptr >= '0' && *ptr <= '9' )
+	    {
+	      int total;
+	      total = (int)(*ptr - '0');
+	      ptr++;
+	      /*octal can only be 3 characters long */
+	      if (*ptr != '\0' &&  (*ptr >= '0' && *ptr <= '9' ) )
+		{
+		  total *= 8;
+		  ptr++;
+		  if (*ptr != '\0' &&  (*ptr >= '0' && *ptr <= '9' ) )
+		    {
+		      total *= 8;
+		      total += (int) (*ptr - '0');
+		      ptr++;
+		    }
+		}
+	      
+	      *retPtr =  (char) total;
+	      retPtr++;
+	    }
+	  
+	  else if (*ptr == 'x')
+	    {
+	      int total;
+	      total = 0;
+	      ptr++;
+	      if (!(*ptr != '\0' &&
+		    ( (*ptr >= '0' && *ptr <= '9' ) ||
+		      (toupper(*ptr) >= (int)('A') && toupper(*ptr) <= (int)('F') ) )
+		      ))
+		{
+		  total = (int)'x';
+		}
+	      else
+		{
+		  while (*ptr != '\0' &&
+		    ( (*ptr >= '0' && *ptr <= '9' ) ||
+		      (toupper(*ptr) >= ((int)('A')) && toupper(*ptr) <= ((int)'F') ) )
+			 )
+		    {
+		      total *= 16;
+		      if (*ptr >= '0' && *ptr <= '9' )
+			total += (int)(*ptr - '0');
+		      else
+			total += ( (toupper(*ptr) - 'A') + 10);
+		      ptr++;
+		    }
+		}
+	      *retPtr =  (char) total;
+	      retPtr++;
+	    }
+	  else
+	    {
+	      switch ( *ptr )
+		{
+		case 'a':
+		  *retPtr = '\a';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+
+		case 'b':
+		  *retPtr = '\b';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+
+		case 'f':
+		  *retPtr = '\f';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+
+		case 'n':
+		  *retPtr = '\n';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+
+		case 'r':
+		  *retPtr = '\r';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+
+		case 't':
+		  *retPtr = '\t';
+		  retPtr++;
+		  /*@switchbreak@*/ break;
+		  /* ' " ? \ */
+		  /* we assume invalid sequences are handled somewhere else
+		     so we handle an invalid sequence of the form \char by replacing
+		     it with char (this is what gcc does) the C standard says a diagnostic is
+		     required..*/
+		default:
+		  *retPtr = *ptr;
+		  retPtr++;
+		}
+	      ptr++;
+	    }
+	  
+	}/*end outer if*/
+      
+    }/*end while */
+
+  /* add the null character */
+  *retPtr = '\0';
+
+  *len = retPtr - ret;
+  return ret;
+}
+
+
+/*this function is like sctring_expandEscapses */
+mstring cstring_expandEscapes (cstring s)
+{
+  int len;
+
+  mstring ret;
+  
+  ret = doExpandEscapes (s, &len);
+  return ret;
+}
+
+int  cstring_lengthExpandEscapes (cstring s)
+{
+  int len;
+
+  mstring tmpStr;
+  
+  tmpStr = doExpandEscapes (s, &len);
+
+  cstring_free(tmpStr);
+
+  return len;
+}
+