/*
** 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
# include "splintMacros.nf"
# include "basic.h"
# include "osd.h"
-# include "portab.h"
/*@only@*/ /*@notnull@*/
cstring cstring_newEmpty (void)
for (i = 0; i < size_toInt (size); i++)
{
- /*drl bee: is*/
+
char c = s[i];
if (strchr (clist, c) != NULL)
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--;
}
}
t++;
}
- /*drl bee: ib*/
- /*drl bee: ib*/
+
if (*s == '\0' && *t != '\0')
{
return CGE_DISTINCT;
else
{
llassert (s != NULL);
- /*drl bee: mrms*/
+
*(s + len) = '\0';
}
cstring sc = cstring_create (len);
strncpy (sc, s, len);
- /*drl bee: mrms*/
+
*(sc + len - 1) = '\0';
*(sc + len - 2) = '.';
*(sc + len - 3) = '.';
{
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;
- /*drl bee: lhnt*/ while ((c = *s) != '\0')
+ while ((c = *s) != '\0')
{
if (c >= 'A' && c <= 'Z')
{
*t++ = c;
s++;
}
- /*drl bee: is*/ *t = '\0';
+ *t = '\0';
return ot;
}
{
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;
return res;
}
-# ifndef NOLCL
/*@only@*/ cstring
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) @*/
if (cstring_isDefined (s))
{
- /*drl bee: sl*/ strcpy (ret, s);
+ strcpy (ret, s);
}
if (cstring_isDefined (t))
{
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))
{
/*@=mayaliasunique@*/
}
- /*drl bee: dm*/ *(s + l + 1) = '\0';
+ *(s + l + 1) = '\0';
return s;
}
-# ifndef NOLCL
bool
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))
}
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;
}
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);
cstring_free (s);
return res;
}
-# endif
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;
if (cstring_isDefined (s)) {
char *t = s;
- /*drl bee: lhnt*/ while (*t != '\0' && isspace ((int) *t)) {
+ while (*t != '\0' && isspace ((int) *t)) {
t++;
}
return cstring_undefined;
}
-/*@i3534 @*/
-/*@ignore@*/ /* !!! DRL don't ignore large segments like this without a good reason! */
-
/* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/
/* This function understands that "sdf\" \"sdfsdf" is okay*/
static mstring doMergeString (cstring s)
retPtr++;
*retPtr = '\0';
BADEXIT;
- return ret;
+
+ /*@notreached@*/ return ret;
}
else
{
ptr++;
}/* end while */
- retPtr = '\0';
+ *retPtr = '\0';
return ret;
}
/* add the null character */
*retPtr = '\0';
- *len = retPtr - ret;
+ llassert( (retPtr-ret) >= 0 );
+ *len = (size_t)(retPtr - ret);
return ret;
}
return c;
}
-/*@end@*/
+