/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 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
** 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
* - cstring_replaceAll () needed in cpplib.c
*/
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
# include "osd.h"
# include "portab.h"
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;
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))
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));
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))
{
}
}
-/*@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);
** Replaces all occurances of old in s with new.
*/
-# if defined (WIN32) || defined (OS2)
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);
{
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')
*sp = *(sp + lendiff);
sp++;
}
-
+
*sp = '\0';
}
sp = strstr (s, old);
}
- }
+ }
}
/*
for (i = 0; i < size; i++)
{
- char c = s[i];
+/*drl bee: is*/ char c = s[i];
if (strchr (clist, c) != NULL)
{
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--;
}
}
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))
t++;
}
+ /*drl bee: ib*/
+ /*drl bee: ib*/
if (*s == '\0' && *t != '\0')
{
return CGE_DISTINCT;
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);
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);
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)
}
cstring
-cstring_capitalize (cstring s)
+cstring_capitalize (cstring s) /*@requires maxSet(s) >= 0 @*/
{
if (!cstring_isEmpty (s))
{
}
cstring
-cstring_capitalizeFree (cstring s)
+cstring_capitalizeFree (cstring s) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @*/
{
if (!cstring_isEmpty (s))
{
else
{
llassert (s != NULL);
- *(s + len) = '\0';
+ /*drl bee: mrms*/ *(s + len) = '\0';
}
return s;
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) = '.';
}
/*@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;
{
for (i = 0; i < n; i++)
{
+ /*drl bee: is*/
+ /*drl bee: is*/
*t++ = *s++;
}
*t = '\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';
cstring ot = t;
char c;
- while ((c = *s) != '\0')
+ /*drl bee: lhnt*/ while ((c = *s) != '\0')
{
if (c >= 'A' && c <= 'Z')
{
*t++ = c;
s++;
}
- *t = '\0';
+ /*drl bee: is*/ *t = '\0';
return ot;
}
{
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;
# 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);
}
/*@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))
{
int l = cstring_length (s1);
char *s = (char *) dmalloc (sizeof (*s) * (l + 2));
- *(s) = c;
+/*drl bee: dm*/ *(s) = c;
if (cstring_isDefined (s1))
{
/*@=mayaliasunique@*/
}
- *(s + l + 1) = '\0';
+ /*drl bee: dm*/ *(s + l + 1) = '\0';
return 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))
{
char *s = dmalloc (sizeof (*s) * (n + 1));
- *s = '\0';
+ /*drl bee: dm*/ *s = '\0';
return s;
}
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;
if (cstring_isDefined (s)) {
char *t = s;
- while (*t != '\0' && isspace ((int) *t)) {
+ /*drl bee: lhnt*/ while (*t != '\0' && isspace ((int) *t)) {
t++;
}
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;
+}
+
andersk / splint.git / blobdiff