X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/393e573f66358664fa7ad34c3436b8395ebc758a..91b588dea2cd9d465b092f5a934ebf1638f79253:/src/cstring.c diff --git a/src/cstring.c b/src/cstring.c index 3408eaf..eeb5f2b 100644 --- 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 @@ -34,7 +34,6 @@ # include "splintMacros.nf" # include "basic.h" # include "osd.h" -# include "portab.h" /*@only@*/ /*@notnull@*/ cstring cstring_newEmpty (void) @@ -265,7 +264,7 @@ void cstring_stripChars (cstring s, const char *clist) for (i = 0; i < size_toInt (size); i++) { - /*drl bee: is*/ + char c = s[i]; if (strchr (clist, c) != NULL) @@ -277,10 +276,10 @@ void cstring_stripChars (cstring s, const char *clist) 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--; } } @@ -375,8 +374,7 @@ cmpcode cstring_genericEqual (cstring s, cstring t, t++; } - /*drl bee: ib*/ - /*drl bee: ib*/ + if (*s == '\0' && *t != '\0') { return CGE_DISTINCT; @@ -592,7 +590,7 @@ cstring_clip (cstring s, size_t len) else { llassert (s != NULL); - /*drl bee: mrms*/ + *(s + len) = '\0'; } @@ -611,7 +609,7 @@ cstring_elide (cstring s, size_t len) cstring sc = cstring_create (len); strncpy (sc, s, len); - /*drl bee: mrms*/ + *(sc + len - 1) = '\0'; *(sc + len - 2) = '.'; *(sc + len - 3) = '.'; @@ -633,8 +631,7 @@ cstring_fill (cstring s, size_t n) /*@requires n >= 0 @*/ { for (i = 0; i < n; i++) { - /*drl bee: is*/ - /*drl bee: is*/ + *t++ = *s++; } *t = '\0'; @@ -643,13 +640,12 @@ cstring_fill (cstring s, size_t 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'; @@ -667,7 +663,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') { @@ -676,7 +672,7 @@ cstring_downcase (cstring s) *t++ = c; s++; } - /*drl bee: is*/ *t = '\0'; + *t = '\0'; return ot; } @@ -698,13 +694,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; @@ -727,7 +723,6 @@ cstring_concatFree1 (cstring s, cstring t) return res; } -# ifndef NOLCL /*@only@*/ cstring cstring_concatChars (cstring s, char *t) { @@ -735,7 +730,6 @@ cstring_concatChars (cstring s, char *t) cstring_free (s); return res; } -# endif /*@only@*/ cstring cstring_concatLength (cstring s1, char *s2, size_t len) /*@requires maxSet(s2) >= (len - 1) @*/ @@ -755,7 +749,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)) { @@ -780,7 +774,7 @@ cstring_prependChar (char c, /*@temp@*/ cstring 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)) { @@ -789,11 +783,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) { @@ -801,7 +794,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)) @@ -813,14 +806,13 @@ cstring_hasNonAlphaNumBar (cstring s) } return FALSE; } -# endif /*@only@*/ /*@notnull@*/ cstring cstring_create (size_t n) { char *s = dmalloc (sizeof (*s) * (n + 1)); - /*drl bee: dm*/ *s = '\0'; + *s = '\0'; return s; } @@ -832,11 +824,10 @@ cstring_copySegment (cstring s, size_t findex, size_t tindex) 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); @@ -844,7 +835,6 @@ lsymbol cstring_toSymbol (cstring s) cstring_free (s); return res; } -# endif cstring cstring_bsearch (cstring key, char **table, int nentries) { @@ -886,7 +876,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; @@ -900,7 +890,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++; } @@ -910,9 +900,6 @@ extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s) return cstring_undefined; } -/*@i3534 @*/ -/*@ignore@*/ - /* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/ /* This function understands that "sdf\" \"sdfsdf" is okay*/ static mstring doMergeString (cstring s) @@ -965,7 +952,8 @@ static mstring doMergeString (cstring s) retPtr++; *retPtr = '\0'; BADEXIT; - return ret; + + /*@notreached@*/ return ret; } else { @@ -981,16 +969,15 @@ static mstring doMergeString (cstring s) ptr++; }/* end while */ - retPtr = '\0'; + *retPtr = '\0'; 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)); @@ -1124,7 +1111,8 @@ static mstring doExpandEscapes (cstring s, /*@out@*/ int * len) /* add the null character */ *retPtr = '\0'; - *len = retPtr - ret; + llassert( (retPtr-ret) >= 0 ); + *len = (size_t)(retPtr - ret); return ret; } @@ -1132,23 +1120,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); @@ -1156,8 +1141,6 @@ int cstring_lengthExpandEscapes (cstring s) return len; } - - cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar) { char *ptr; @@ -1179,7 +1162,6 @@ cstring cstring_replaceChar(/*@returned@*/ cstring c, char oldChar, char newChar return c; } -/*@end@*/