2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
30 * - use drive spec specials with OS2 like with WIN32
31 * - cstring_replaceAll () needed in cpplib.c
34 # include "splintMacros.nf"
39 /*@only@*/ /*@notnull@*/
40 cstring cstring_newEmpty (void)
42 return (cstring_create (0));
45 char cstring_firstChar (cstring s)
47 llassert (cstring_isDefined (s));
48 llassert (cstring_length (s) > 0);
53 char cstring_getChar (cstring s, int n)
55 int length = cstring_length (s);
57 llassert (cstring_isDefined (s));
58 llassert (n >= 1 && n <= length);
63 cstring cstring_suffix (cstring s, int n)
65 llassert (cstring_isDefined (s));
66 llassert (n <= cstring_length (s));
71 cstring cstring_prefix (cstring s, int n) /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/ /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
75 llassert (cstring_isDefined (s));
76 llassert (n <= cstring_length (s));
79 /*@-mods@*/ /* The modifications cancel out. */
88 /* effects If s = [0-9]*, returns s as an int.
92 int cstring_toPosInt (cstring s)
98 if (isdigit ((unsigned char) c))
100 val = (val * 10) + (int)(c - '0');
106 } end_cstring_chars ;
111 cstring cstring_afterChar (cstring s, char c)
113 llassert (cstring_isDefined (s));
114 return strchr (s, c);
117 cstring cstring_beforeChar (cstring s, char c)
119 if (cstring_isDefined (s))
121 char *cp = strchr (s, c);
129 ret = cstring_copy (s);
131 /*@=mods@*/ /* modification is undone */
137 return cstring_undefined;
140 void cstring_setChar (cstring s, int n, char c) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
142 llassert (cstring_isDefined (s));
143 llassert (n > 0 && n <= cstring_length (s));
148 char cstring_lastChar (cstring s)
152 llassert (cstring_isDefined (s));
154 length = cstring_length (s);
155 llassert (length > 0);
157 return (s[length - 1]);
160 /*@only@*/ cstring cstring_copy (cstring s) /*@ensures maxSet(result) == maxRead(s) /\ maxRead(result) == maxRead(s) @*/
162 if (cstring_isDefined (s))
164 return (mstring_copy (s));
168 return cstring_undefined;
172 /*@only@*/ cstring cstring_copyLength (char *s, int len) /*@requires maxSet(s) >= (len - 1) @*/
174 char *res = mstring_create (len + 1);
176 strncpy (res, s, size_fromInt (len));
181 bool cstring_containsChar (cstring c, char ch)
183 if (cstring_isDefined (c))
185 return (strchr (c, ch) != NULL);
194 ** Replaces all occurances of old in s with new.
197 void cstring_replaceAll (cstring s, char old, char snew)
200 llassert (old != snew);
202 if (cstring_isDefined (s))
204 char *sp = strchr (s, old);
209 sp = strchr (sp, old);
215 void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) /*@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @*/
218 llassert (strlen (old) >= strlen (snew));
220 if (cstring_isDefined (s))
222 char *sp = strstr (s, old);
226 int lendiff = size_toInt (strlen (old) - strlen (snew));
229 while (*tsnew != '\0')
236 while (*(sp + lendiff) != '\0')
238 *sp = *(sp + lendiff);
245 sp = strstr (s, old);
251 ** removes all chars in clist from s
254 void cstring_stripChars (cstring s, const char *clist)
256 if (cstring_isDefined (s))
259 int size = cstring_length (s);
261 for (i = 0; i < size; i++)
263 /*drl bee: is*/ char c = s[i];
265 if (strchr (clist, c) != NULL)
267 /* strip this char */
272 for (j = i; j < size; j++)
274 /*drl bee: is*/ /*drl bee: is*/ s[j] = s[j+1];
277 /*drl bee: is*/ s[size] = '\0';
284 bool cstring_contains (/*@unique@*/ cstring c, cstring sub)
286 if (cstring_isDefined (c))
288 llassert (cstring_isDefined (sub));
290 return (strstr (c, sub) != NULL);
298 static char lookLike (char c) /*@*/
300 if (c == 'I' || c == 'l')
304 else if (c == 'O' || c == 'o')
322 cmpcode cstring_genericEqual (cstring s, cstring t,
324 bool caseinsensitive,
325 bool lookalike) /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
327 if (s == t) return CGE_SAME;
328 else if (cstring_isUndefined (s))
330 return cstring_isEmpty (t) ? CGE_SAME : CGE_DISTINCT;
332 else if (cstring_isUndefined (t))
334 return cstring_isEmpty (s) ? CGE_SAME : CGE_DISTINCT;
339 bool diffcase = FALSE;
340 bool difflookalike = FALSE;
344 if (nchars > 0 && i >= nchars)
351 ; /* no difference */
353 else if (caseinsensitive
354 && (toupper ((int) *t) == toupper ((int) *s)))
358 else if (lookalike && (lookLike (*t) == lookLike (*s)))
360 difflookalike = TRUE;
373 if (*s == '\0' && *t != '\0')
382 else if (difflookalike)
384 return CGE_LOOKALIKE;
395 bool cstring_equalFree (/*@only@*/ cstring c1, /*@only@*/ cstring c2)
397 bool res = cstring_equal (c1, c2);
403 bool cstring_equal (cstring c1, cstring c2)
405 if (c1 == c2) return TRUE;
406 else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
407 else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
408 else return (strcmp (c1, c2) == 0);
411 bool cstring_equalLen (cstring c1, cstring c2, int len)
413 if (c1 == c2) return TRUE;
414 else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
415 else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
416 else return (strncmp (c1, c2, size_fromInt (len)) == 0);
419 bool cstring_equalCaseInsensitive (cstring c1, cstring c2)
421 if (c1 == c2) return TRUE;
422 else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
423 else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
424 else return (cstring_genericEqual (c1, c2, 0, TRUE, FALSE) != CGE_DISTINCT);
427 bool cstring_equalLenCaseInsensitive (cstring c1, cstring c2, int len)
431 if (c1 == c2) return TRUE;
432 else if (cstring_isUndefined (c1)) return cstring_isEmpty (c2);
433 else if (cstring_isUndefined (c2)) return cstring_isEmpty (c1);
434 else return (cstring_genericEqual (c1, c2, len, TRUE, FALSE) != CGE_DISTINCT);
437 bool cstring_equalPrefix (cstring c1, cstring c2)
439 llassert (c2 != NULL);
441 if (cstring_isUndefined (c1))
443 return (strlen (c2) == 0);
446 return (strncmp (c1, c2, strlen (c2)) == 0);
449 bool cstring_equalPrefixLit (cstring c1, const char *c2)
451 llassert (c2 != NULL);
453 if (cstring_isUndefined (c1))
455 return (strlen (c2) == 0);
458 return (strncmp (c1, c2, strlen (c2)) == 0);
461 int cstring_xcompare (cstring *c1, cstring *c2)
463 return (cstring_compare (*c1, *c2));
466 int cstring_compare (cstring c1, cstring c2)
474 else if (cstring_isUndefined (c1))
476 if (cstring_isEmpty (c2))
485 else if (cstring_isUndefined (c2))
487 if (cstring_isEmpty (c1))
498 res = strcmp (c1, c2);
504 void cstring_markOwned (/*@owned@*/ cstring s)
509 void cstring_free (/*@only@*/ cstring s)
511 if (cstring_isDefined (s))
517 cstring cstring_fromChars (/*@exposed@*/ const char *cp)
522 /*@exposed@*/ char *cstring_toCharsSafe (cstring s)
524 static /*@only@*/ cstring emptystring = cstring_undefined;
526 if (cstring_isDefined (s))
532 if (cstring_isUndefined (emptystring))
534 emptystring = cstring_newEmpty ();
541 int cstring_length (cstring s)
543 if (cstring_isDefined (s))
545 return size_toInt (strlen (s));
551 cstring_capitalize (cstring s) /*@requires maxSet(s) >= 0 @*/
553 if (!cstring_isEmpty (s))
555 cstring ret = cstring_copy (s);
557 cstring_setChar (ret, 1, (char) toupper ((int) cstring_firstChar (ret)));
561 return cstring_undefined;
565 cstring_capitalizeFree (cstring s) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @*/
567 if (!cstring_isEmpty (s))
569 cstring_setChar (s, 1, (char) toupper ((int) cstring_firstChar (s)));
577 cstring_clip (cstring s, int len)
579 if (cstring_isUndefined (s) || cstring_length (s) <= len)
585 llassert (s != NULL);
586 /*drl bee: mrms*/ *(s + len) = '\0';
593 cstring_elide (cstring s, int len)
595 if (cstring_isUndefined (s) || cstring_length (s) <= len)
597 return cstring_copy (s);
601 cstring sc = cstring_create (len);
603 strncpy (sc, s, size_fromInt (len));
604 /*drl bee: mrms*/ *(sc + len - 1) = '\0';
605 *(sc + len - 2) = '.';
606 *(sc + len - 3) = '.';
607 *(sc + len - 4) = '.';
613 cstring_fill (cstring s, int n) /*@requires n >= 0 @*/
615 cstring t = cstring_create (n + 1);
617 int len = cstring_length (s);
622 for (i = 0; i < n; i++)
632 for (i = 0; i < len; i++)
638 for (i = 0; i < n - len; i++)
650 cstring_downcase (cstring s)
652 if (cstring_isDefined (s))
654 cstring t = cstring_create (strlen (s) + 1);
658 /*drl bee: lhnt*/ while ((c = *s) != '\0')
660 if (c >= 'A' && c <= 'Z')
667 /*drl bee: is*/ *t = '\0';
673 return cstring_undefined;
677 /*@notnull@*/ cstring
678 cstring_appendChar (/*@only@*/ cstring s1, char c)
680 int l = cstring_length (s1);
683 s = (char *) dmalloc (sizeof (*s) * (l + 2));
685 if (cstring_isDefined (s1))
689 /*drl bee: dm*/ *(s + l + 1) = '\0';
695 /*drl bee: dm*/ *(s + 1) = '\0';
702 cstring_concatFree (cstring s, cstring t)
704 cstring res = cstring_concat (s, t);
711 cstring_concatFree1 (cstring s, cstring t)
713 cstring res = cstring_concat (s, t);
720 cstring_concatChars (cstring s, char *t)
722 cstring res = cstring_concat (s, cstring_fromChars (t));
729 cstring_concatLength (cstring s1, char *s2, int len) /*@requires maxSet(s2) >= (len - 1) @*/
731 cstring tmp = cstring_copyLength (s2, len);
732 cstring res = cstring_concat (s1, tmp);
740 cstring_concat (cstring s, cstring t) /*@requires maxSet(s) >= 0 @*/
742 char *ret = mstring_create (cstring_length (s) + cstring_length (t));
744 if (cstring_isDefined (s))
746 /*drl bee: sl*/ strcpy (ret, s);
748 if (cstring_isDefined (t))
756 /*@notnull@*/ /*@only@*/ cstring
757 cstring_prependCharO (char c, /*@only@*/ cstring s1)
759 cstring res = cstring_prependChar (c, s1);
765 /*@notnull@*/ /*@only@*/ cstring
766 cstring_prependChar (char c, /*@temp@*/ cstring s1)
768 int l = cstring_length (s1);
769 char *s = (char *) dmalloc (sizeof (*s) * (l + 2));
771 /*drl bee: dm*/ *(s) = c;
773 if (cstring_isDefined (s1))
775 /*@-mayaliasunique@*/
777 /*@=mayaliasunique@*/
780 /*drl bee: dm*/ *(s + l + 1) = '\0';
786 cstring_hasNonAlphaNumBar (cstring s)
790 if (cstring_isUndefined (s)) return FALSE;
792 /*drl bee: lhnt*/ while ((c = (int) *s) != (int) '\0')
794 if ((isalnum (c) == 0) && (c != (int) '_')
795 && (c != (int) '.') && (c != (int) CONNECTCHAR))
806 /*@only@*/ /*@notnull@*/ cstring
807 cstring_create (int n)
809 char *s = dmalloc (sizeof (*s) * (n + 1));
811 /*drl bee: dm*/ *s = '\0';
815 /*@only@*/ /*@notnull@*/ cstring
816 cstring_copySegment (cstring s, int findex, int tindex)
818 cstring res = cstring_create (tindex - findex + 1);
820 llassert (cstring_isDefined (s));
821 llassert (cstring_length (s) > tindex);
823 strncpy (res, (s + findex), size_fromInt ((tindex - findex + 1)));
828 lsymbol cstring_toSymbol (cstring s)
830 lsymbol res = lsymbol_fromString (s);
837 cstring cstring_bsearch (cstring key, char **table, int nentries)
839 if (cstring_isDefined (key))
843 int mid = (high + low + 1) / 2;
845 cstring res = cstring_undefined;
847 while (low <= high && mid < nentries)
851 llassert (mid != last);
852 llassert (mid >= 0 && mid < nentries);
854 cmp = cstring_compare (key, table[mid]);
861 else if (cmp < 0) /* key is before table[mid] */
865 else /* key of after table[mid] */
871 mid = (high + low + 1) / 2;
874 if (mid != 0 && mid < nentries - 1)
876 llassert (cstring_compare (key, table[mid - 1]) > 0);
877 /*drl bee: ndv*/ llassert (cstring_compare (key, table[mid + 1]) < 0);
883 return cstring_undefined;
886 extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s)
888 if (cstring_isDefined (s)) {
891 /*drl bee: lhnt*/ while (*t != '\0' && isspace ((int) *t)) {
898 return cstring_undefined;