2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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: info@splint.org
21 ** To report a bug: splint-bug@splint.org
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"
38 /*@only@*/ /*@notnull@*/
39 cstring
cstring_newEmpty (void)
41 return (cstring_create (0));
44 char cstring_firstChar (cstring s
)
46 llassert (cstring_isDefined (s
));
47 llassert (cstring_length (s
) > 0);
52 char cstring_getChar (cstring s
, size_t n
)
54 size_t length
= cstring_length (s
);
56 llassert (cstring_isDefined (s
));
57 llassert (n
>= 1 && n
<= length
);
62 cstring
cstring_suffix (cstring s
, size_t n
)
64 llassert (cstring_isDefined (s
));
65 llassert (n
<= cstring_length (s
));
70 cstring
cstring_prefix (cstring s
, size_t n
)
71 /*@requires maxRead(s) >= n /\ maxSet(s) >= n @*/
72 /*@ensures maxRead(result) == n /\ maxSet(result) == n @*/
76 llassert (cstring_isDefined (s
));
77 llassert (n
<= cstring_length (s
));
80 /*@-mods@*/ /* The modifications cancel out. */
89 /* effects If s = [0-9]*, returns s as an int.
93 int cstring_toPosInt (cstring s
)
99 if (isdigit ((unsigned char) c
))
101 val
= (val
* 10) + (int)(c
- '0');
107 } end_cstring_chars
;
112 cstring
cstring_afterChar (cstring s
, char c
)
114 llassert (cstring_isDefined (s
));
115 return strchr (s
, c
);
118 cstring
cstring_beforeChar (cstring s
, char c
)
120 if (cstring_isDefined (s
))
122 char *cp
= strchr (s
, c
);
130 ret
= cstring_copy (s
);
132 /*@=mods@*/ /* modification is undone */
138 return cstring_undefined
;
141 void cstring_setChar (cstring s
, size_t n
, char c
) /*@requires maxRead(s) >= (n - 1) /\ maxSet(s) >= (n - 1) @*/
143 llassert (cstring_isDefined (s
));
144 llassert (n
> 0 && n
<= cstring_length (s
));
149 char cstring_lastChar (cstring s
)
153 llassert (cstring_isDefined (s
));
155 length
= cstring_length (s
);
156 llassert (length
> 0);
158 return (s
[length
- 1]);
161 /*@only@*/ cstring
cstring_copy (cstring s
) /*@ensures maxSet(result) == maxRead(s) /\ maxRead(result) == maxRead(s) @*/
163 if (cstring_isDefined (s
))
165 return (mstring_copy (s
));
169 return cstring_undefined
;
173 /*@only@*/ cstring
cstring_copyLength (char *s
, size_t len
) /*@requires maxSet(s) >= (len - 1) @*/
175 char *res
= mstring_create (len
+ 1);
177 strncpy (res
, s
, len
);
182 bool cstring_containsChar (cstring c
, char ch
)
184 if (cstring_isDefined (c
))
186 return (strchr (c
, ch
) != NULL
);
195 ** Replaces all occurances of old in s with new.
198 void cstring_replaceAll (cstring s
, char old
, char snew
)
201 llassert (old
!= snew
);
203 if (cstring_isDefined (s
))
205 char *sp
= strchr (s
, old
);
210 sp
= strchr (sp
, old
);
216 void cstring_replaceLit (/*@unique@*/ cstring s
, char *old
, char *snew
)
217 /*@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @*/
219 llassert (strlen (old
) >= strlen (snew
));
221 if (cstring_isDefined (s
))
223 char *sp
= strstr (s
, old
);
227 int lendiff
= size_toInt (strlen (old
) - strlen (snew
));
230 llassert (lendiff
>= 0);
232 while (*tsnew
!= '\0')
234 llassert (*sp
!= '\0');
240 while (*(sp
+ lendiff
) != '\0')
242 *sp
= *(sp
+ lendiff
);
249 sp
= strstr (s
, old
);
255 ** removes all chars in clist from s
258 void cstring_stripChars (cstring s
, const char *clist
)
260 if (cstring_isDefined (s
))
263 size_t size
= cstring_length (s
);
265 for (i
= 0; i
< size_toInt (size
); i
++)
270 if (strchr (clist
, c
) != NULL
)
272 /* strip this char */
277 for (j
= i
; j
< size_toInt (size
); j
++)
289 bool cstring_contains (/*@unique@*/ cstring c
, cstring sub
)
291 if (cstring_isDefined (c
))
293 llassert (cstring_isDefined (sub
));
295 return (strstr (c
, sub
) != NULL
);
303 static char lookLike (char c
) /*@*/
305 if (c
== 'I' || c
== 'l')
309 else if (c
== 'O' || c
== 'o')
327 cmpcode
cstring_genericEqual (cstring s
, cstring t
,
329 bool caseinsensitive
,
331 /*@requires maxRead(s) >= nchars /\ maxRead(t) >= nchars @*/
333 if (s
== t
) return CGE_SAME
;
334 else if (cstring_isUndefined (s
))
336 return cstring_isEmpty (t
) ? CGE_SAME
: CGE_DISTINCT
;
338 else if (cstring_isUndefined (t
))
340 return cstring_isEmpty (s
) ? CGE_SAME
: CGE_DISTINCT
;
345 bool diffcase
= FALSE
;
346 bool difflookalike
= FALSE
;
350 if (nchars
> 0 && i
>= size_toInt (nchars
))
357 ; /* no difference */
359 else if (caseinsensitive
360 && (toupper ((int) *t
) == toupper ((int) *s
)))
364 else if (lookalike
&& (lookLike (*t
) == lookLike (*s
)))
366 difflookalike
= TRUE
;
378 if (*s
== '\0' && *t
!= '\0')
387 else if (difflookalike
)
389 return CGE_LOOKALIKE
;
400 bool cstring_equalFree (/*@only@*/ cstring c1
, /*@only@*/ cstring c2
)
402 bool res
= cstring_equal (c1
, c2
);
408 bool cstring_equal (cstring c1
, cstring c2
)
410 if (c1
== c2
) return TRUE
;
411 else if (cstring_isUndefined (c1
)) return cstring_isEmpty (c2
);
412 else if (cstring_isUndefined (c2
)) return cstring_isEmpty (c1
);
413 else return (strcmp (c1
, c2
) == 0);
416 bool cstring_equalLen (cstring c1
, cstring c2
, size_t len
)
418 if (c1
== c2
) return TRUE
;
419 else if (cstring_isUndefined (c1
)) return cstring_isEmpty (c2
);
420 else if (cstring_isUndefined (c2
)) return cstring_isEmpty (c1
);
421 else return (strncmp (c1
, c2
, len
) == 0);
424 bool cstring_equalCaseInsensitive (cstring c1
, cstring c2
)
426 if (c1
== c2
) return TRUE
;
427 else if (cstring_isUndefined (c1
)) return cstring_isEmpty (c2
);
428 else if (cstring_isUndefined (c2
)) return cstring_isEmpty (c1
);
429 else return (cstring_genericEqual (c1
, c2
, 0, TRUE
, FALSE
) != CGE_DISTINCT
);
432 bool cstring_equalLenCaseInsensitive (cstring c1
, cstring c2
, size_t len
)
434 if (c1
== c2
) return TRUE
;
435 else if (cstring_isUndefined (c1
)) return cstring_isEmpty (c2
);
436 else if (cstring_isUndefined (c2
)) return cstring_isEmpty (c1
);
437 else return (cstring_genericEqual (c1
, c2
, len
, TRUE
, FALSE
) != CGE_DISTINCT
);
440 bool cstring_equalPrefix (cstring c1
, cstring c2
)
442 llassert (c2
!= NULL
);
444 if (cstring_isUndefined (c1
))
446 return (strlen (c2
) == 0);
449 return (strncmp (c1
, c2
, strlen (c2
)) == 0);
452 bool cstring_equalPrefixLit (cstring c1
, const char *c2
)
454 llassert (c2
!= NULL
);
456 if (cstring_isUndefined (c1
))
458 return (strlen (c2
) == 0);
461 return (strncmp (c1
, c2
, strlen (c2
)) == 0);
464 int cstring_xcompare (cstring
*c1
, cstring
*c2
)
466 return (cstring_compare (*c1
, *c2
));
469 int cstring_compare (cstring c1
, cstring c2
)
477 else if (cstring_isUndefined (c1
))
479 if (cstring_isEmpty (c2
))
488 else if (cstring_isUndefined (c2
))
490 if (cstring_isEmpty (c1
))
501 res
= strcmp (c1
, c2
);
507 void cstring_markOwned (/*@owned@*/ cstring s
)
512 void cstring_free (/*@only@*/ cstring s
)
514 if (cstring_isDefined (s
))
523 cstring
cstring_fromChars (/*@exposed@*/ const char *cp
)
528 /*@exposed@*/ char *cstring_toCharsSafe (cstring s
)
530 static /*@only@*/ cstring emptystring
= cstring_undefined
;
532 if (cstring_isDefined (s
))
538 if (cstring_isUndefined (emptystring
))
540 emptystring
= cstring_newEmpty ();
547 size_t cstring_length (cstring s
)
549 if (cstring_isDefined (s
))
558 cstring_capitalize (cstring s
) /*@requires maxSet(s) >= 0 @*/
560 if (!cstring_isEmpty (s
))
562 cstring ret
= cstring_copy (s
);
564 cstring_setChar (ret
, 1, (char) toupper ((int) cstring_firstChar (ret
)));
568 return cstring_undefined
;
572 cstring_capitalizeFree (cstring s
) /*@requires maxSet(s) >= 0 /\ maxRead(s) >= 0 @*/
574 if (!cstring_isEmpty (s
))
576 cstring_setChar (s
, 1, (char) toupper ((int) cstring_firstChar (s
)));
584 cstring_clip (cstring s
, size_t len
)
586 if (cstring_isUndefined (s
) || cstring_length (s
) <= len
)
592 llassert (s
!= NULL
);
601 cstring_elide (cstring s
, size_t len
)
603 if (cstring_isUndefined (s
) || cstring_length (s
) <= len
)
605 return cstring_copy (s
);
609 cstring sc
= cstring_create (len
);
611 strncpy (sc
, s
, len
);
613 *(sc
+ len
- 1) = '\0';
614 *(sc
+ len
- 2) = '.';
615 *(sc
+ len
- 3) = '.';
616 *(sc
+ len
- 4) = '.';
623 cstring_fill (cstring s
, size_t n
) /*@requires n >= 0 @*/
625 cstring t
= cstring_create (n
+ 1);
627 size_t len
= cstring_length (s
);
632 for (i
= 0; i
< n
; i
++)
641 for (i
= 0; i
< len
; i
++)
646 for (i
= 0; i
< n
- len
; i
++)
658 cstring_downcase (cstring s
)
660 if (cstring_isDefined (s
))
662 cstring t
= cstring_create (strlen (s
) + 1);
666 while ((c
= *s
) != '\0')
668 if (c
>= 'A' && c
<= 'Z')
681 return cstring_undefined
;
685 /*@notnull@*/ cstring
686 cstring_appendChar (/*@only@*/ cstring s1
, char c
)
688 size_t l
= cstring_length (s1
);
691 s
= (char *) dmalloc (sizeof (*s
) * (l
+ 2));
693 if (cstring_isDefined (s1
))
710 cstring_concatFree (cstring s
, cstring t
)
712 cstring res
= cstring_concat (s
, t
);
719 cstring_concatFree1 (cstring s
, cstring t
)
721 cstring res
= cstring_concat (s
, t
);
727 cstring_concatChars (cstring s
, char *t
)
729 cstring res
= cstring_concat (s
, cstring_fromChars (t
));
735 cstring_concatLength (cstring s1
, char *s2
, size_t len
) /*@requires maxSet(s2) >= (len - 1) @*/
737 cstring tmp
= cstring_copyLength (s2
, len
);
738 cstring res
= cstring_concat (s1
, tmp
);
746 cstring_concat (cstring s
, cstring t
) /*@requires maxSet(s) >= 0 @*/
748 char *ret
= mstring_create (cstring_length (s
) + cstring_length (t
));
750 if (cstring_isDefined (s
))
754 if (cstring_isDefined (t
))
762 /*@notnull@*/ /*@only@*/ cstring
763 cstring_prependCharO (char c
, /*@only@*/ cstring s1
)
765 cstring res
= cstring_prependChar (c
, s1
);
771 /*@notnull@*/ /*@only@*/ cstring
772 cstring_prependChar (char c
, /*@temp@*/ cstring s1
)
774 size_t l
= cstring_length (s1
);
775 char *s
= (char *) dmalloc (sizeof (*s
) * (l
+ 2));
779 if (cstring_isDefined (s1
))
781 /*@-mayaliasunique@*/
783 /*@=mayaliasunique@*/
791 cstring_hasNonAlphaNumBar (cstring s
)
795 if (cstring_isUndefined (s
)) return FALSE
;
797 while ((c
= (int) *s
) != (int) '\0')
799 if ((isalnum (c
) == 0) && (c
!= (int) '_')
800 && (c
!= (int) '.') && (c
!= (int) CONNECTCHAR
))
810 /*@only@*/ /*@notnull@*/ cstring
811 cstring_create (size_t n
)
813 char *s
= dmalloc (sizeof (*s
) * (n
+ 1));
819 /*@only@*/ /*@notnull@*/ cstring
820 cstring_copySegment (cstring s
, size_t findex
, size_t tindex
)
822 cstring res
= cstring_create (tindex
- findex
+ 1);
824 llassert (cstring_isDefined (s
));
825 llassert (cstring_length (s
) > tindex
);
827 strncpy (res
, (s
+ findex
), size_fromInt (size_toInt (tindex
- findex
) + 1));
831 lsymbol
cstring_toSymbol (cstring s
)
833 lsymbol res
= lsymbol_fromString (s
);
839 cstring
cstring_bsearch (cstring key
, char **table
, int nentries
)
841 if (cstring_isDefined (key
))
845 int mid
= (high
+ low
+ 1) / 2;
847 cstring res
= cstring_undefined
;
849 while (low
<= high
&& mid
< nentries
)
853 llassert (mid
!= last
);
854 llassert (mid
>= 0 && mid
< nentries
);
856 cmp
= cstring_compare (key
, table
[mid
]);
863 else if (cmp
< 0) /* key is before table[mid] */
867 else /* key of after table[mid] */
873 mid
= (high
+ low
+ 1) / 2;
876 if (mid
!= 0 && mid
< nentries
- 1)
878 llassert (cstring_compare (key
, table
[mid
- 1]) > 0);
879 llassert (cstring_compare (key
, table
[mid
+ 1]) < 0);
885 return cstring_undefined
;
888 extern /*@observer@*/ cstring
cstring_advanceWhiteSpace (cstring s
)
890 if (cstring_isDefined (s
)) {
893 while (*t
!= '\0' && isspace ((int) *t
)) {
900 return cstring_undefined
;
903 /* changes strings like "sdf" "sdfsd" into "sdfsdfsd"*/
904 /* This function understands that "sdf\" \"sdfsdf" is okay*/
905 static mstring
doMergeString (cstring s
)
912 llassert(cstring_isDefined (s
));
914 ret
= mstring_create (cstring_length(s
) );
920 llassert(*ptr == '\"');
939 /* case of escaped \ ('\\') */
942 else if ( (*ptr
== '\"') && (!escape
) )
944 while ( (ptr
[1] != '\"') && (ptr
[1] != '\0') )
950 llassert(*ptr
== '\"');
956 /*@notreached@*/ return ret
;
976 static mstring
doExpandEscapes (cstring s
, /*@out@*/ size_t *len
)
982 llassert(cstring_isDefined (s
));
984 ret
= mstring_create (cstring_length(s
));
1004 /*not a legal escape sequence but try to handle it in a sesible way*/
1009 /* Handle Octal escapes */
1010 else if (*ptr
>= '0' && *ptr
<= '9' )
1013 total
= (int)(*ptr
- '0');
1015 /*octal can only be 3 characters long */
1016 if (*ptr
!= '\0' && (*ptr
>= '0' && *ptr
<= '9' ) )
1020 if (*ptr
!= '\0' && (*ptr
>= '0' && *ptr
<= '9' ) )
1023 total
+= (int) (*ptr
- '0');
1028 *retPtr
= (char) total
;
1032 else if (*ptr
== 'x')
1037 if (!(*ptr
!= '\0' &&
1038 ( (*ptr
>= '0' && *ptr
<= '9' ) ||
1039 (toupper(*ptr
) >= (int)('A') && toupper(*ptr
) <= (int)('F') ) )
1046 while (*ptr
!= '\0' &&
1047 ( (*ptr
>= '0' && *ptr
<= '9' ) ||
1048 (toupper(*ptr
) >= ((int)('A')) && toupper(*ptr
) <= ((int)'F') ) )
1052 if (*ptr
>= '0' && *ptr
<= '9' )
1053 total
+= (int)(*ptr
- '0');
1055 total
+= ( (toupper(*ptr
) - 'A') + 10);
1059 *retPtr
= (char) total
;
1069 /*@switchbreak@*/ break;
1074 /*@switchbreak@*/ break;
1079 /*@switchbreak@*/ break;
1084 /*@switchbreak@*/ break;
1089 /*@switchbreak@*/ break;
1094 /*@switchbreak@*/ break;
1096 /* we assume invalid sequences are handled somewhere else
1097 so we handle an invalid sequence of the form \char by replacing
1098 it with char (this is what gcc does) the C standard says a diagnostic is
1111 /* add the null character */
1114 llassert( (retPtr
-ret
) >= 0 );
1115 *len
= (size_t)(retPtr
- ret
);
1120 /*this function is like sctring_expandEscapses */
1121 mstring
cstring_expandEscapes (cstring s
)
1126 ret
= doExpandEscapes (s
, &len
);
1130 size_t cstring_lengthExpandEscapes (cstring s
)
1133 mstring tmpStr
, tmpStr2
;
1135 tmpStr
= doMergeString (s
);
1136 tmpStr2
= doExpandEscapes (tmpStr
, &len
);
1138 cstring_free(tmpStr
);
1139 cstring_free(tmpStr2
);
1144 cstring
cstring_replaceChar(/*@returned@*/ cstring c
, char oldChar
, char newChar
)
1147 llassert(oldChar
!= '\0');
1148 if (cstring_isUndefined(c
) )
1150 llcontbug(cstring_makeLiteral("cstring_replaceChar called with undefined string"));
1155 while (*ptr
!= '\0')
1157 if (*ptr
== oldChar
)