From 805dcfa90e8bc7e29aba8082845007921832db37 Mon Sep 17 00:00:00 2001 From: Mihail Groza Date: Tue, 31 Jan 2017 21:43:40 +0000 Subject: [PATCH] Minor fixes for glitches in cstring. --- src/Headers/cstring.h | 53 +++++++++++++++++++++++++++++++++------------------ src/cstring.c | 40 ++++++++++++++++++++++++++------------ 2 files changed, 62 insertions(+), 31 deletions(-) diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h index a31227e..b15a0a3 100644 --- a/src/Headers/cstring.h +++ b/src/Headers/cstring.h @@ -12,19 +12,25 @@ /* typedefs in forwardTypes */ -extern /*@notnull@*/ cstring cstring_create (size_t p_n) /*@*/ /*@ensures maxSet(result) == p_n @*/ ; +extern /*@notnull@*/ cstring cstring_create (size_t p_n) + /*@*/ + /*@ensures maxSet(result) == p_n @*/ ; extern /*@only@*/ /*@notnull@*/ cstring cstring_newEmpty (void) ; extern /*@notnull@*/ cstring cstring_appendChar (/*@only@*/ cstring p_s1, char p_c); -extern cstring cstring_concatLength (/*@only@*/ cstring p_s1, char *p_s2, size_t p_len) +extern cstring cstring_concatLength (/*@only@*/ cstring p_s1, const char *p_s2, size_t p_len) /*@*/ /*@requires maxSet(p_s2) >= (p_len - 1) @*/ ; extern /*@notnull@*/ cstring cstring_prependChar (char p_c, /*@temp@*/ cstring p_s1); extern /*@notnull@*/ cstring cstring_prependCharO (char p_c, /*@only@*/ cstring p_s1); extern cstring cstring_downcase (cstring p_s) /*@*/ ; -extern cstring cstring_copy (cstring p_s) /*@*/ /*@ensures maxSet(result) == maxRead(p_s) /\ maxRead(result) == maxRead(p_s) @*/ ; -extern cstring cstring_copyLength (char *p_s, size_t p_len) /*@*/ /*@requires maxSet(p_s) >= (p_len - 1) @*/; +extern cstring cstring_copy (cstring p_s) + /*@*/ + /*@ensures maxSet(result) == maxRead(p_s) /\ maxRead(result) == maxRead(p_s) @*/ ; +extern cstring cstring_copyLength (const char *p_s, size_t p_len) + /*@*/ + /*@requires maxSet(p_s) >= (p_len - 1) @*/; extern int cstring_toPosInt (cstring p_s) /*@*/ ; @@ -59,10 +65,11 @@ extern void cstring_setChar (cstring p_s, size_t p_n, char p_c) # define cstring_secondChar(s) cstring_getChar (s, 2) extern /*@exposed@*/ /*@notnull@*/ /*@untainted@*/ char * -cstring_toCharsSafe (/*@temp@*/ /*@exposed@*/ /*@returned@*/ cstring p_s) - /*@*/ ; +cstring_toCharsSafe (/*@temp@*/ /*@exposed@*/ /*@returned@*/ cstring p_s) /*@*/ ; -extern size_t cstring_length (cstring p_s) /*@*/ /*@ensures result == maxRead(p_s) @*/; +extern size_t cstring_length (cstring p_s) + /*@*/ + /*@ensures result == maxRead(p_s) @*/; extern bool cstring_contains (/*@unique@*/ cstring p_c, cstring p_sub) /*@*/ ; extern bool cstring_containsChar (cstring p_c, char p_ch) /*@*/ ; @@ -72,7 +79,7 @@ extern bool cstring_equalLen (cstring p_c1, cstring p_c2, size_t p_len) /*@*/ ; extern bool cstring_equalLenCaseInsensitive (cstring p_c1, cstring p_c2, size_t p_len) /*@*/ ; extern bool cstring_equalPrefix (cstring p_c1, cstring p_c2) /*@*/ ; extern bool cstring_equalPrefixLit (cstring p_c1, /*@observer@*/ const char *p_c2) /*@*/ ; -extern bool cstring_equalLit (cstring p_c1, char *p_c2) /*@*/ ; +extern bool cstring_equalLit (cstring p_c1, const char *p_c2) /*@*/ ; extern int cstring_compare (cstring p_c1, cstring p_c2) /*@*/ ; extern int cstring_xcompare (cstring *p_c1, cstring *p_c2) /*@*/ ; @@ -104,12 +111,12 @@ cstring_fromChars (/*@returned@*/ /*@null@*/ const /*@exposed@*/ /*@temp@*/ char *p_cp) /*@*/ ; extern cstring -cstring_fromCharsO (/*@null@*/ /*@only@*/ char *p_cp) /*@*/ ; +cstring_fromCharsO (const /*@null@*/ /*@only@*/ char *p_cp) /*@*/ ; /*@-mustfree@*/ # define cstring_fromCharsO(s) cstring_fromChars(s) /*@=mustfree@*/ -extern cstring cstring_fromCharsNew (/*@null@*/ char *p_s) /*@*/ ; +extern cstring cstring_fromCharsNew (const /*@null@*/ char *p_s) /*@*/ ; # define cstring_fromCharsNew(s) cstring_copy(cstring_fromChars(s)) extern /*@exposed@*/ /*@notnull@*/ /*@untainted@*/ @@ -135,17 +142,23 @@ extern /*@falsewhennull@*/ bool cstring_isNonEmpty (cstring p_s) /*@*/ ; # define cstring_isEmpty(s) (cstring_length(s) == 0) # define cstring_isNonEmpty(s) (!cstring_isEmpty(s)) -extern cstring cstring_makeLiteral (char *) /*@*/ ; +extern cstring cstring_makeLiteral (const char *) /*@*/ ; extern /*@observer@*/ /*@dependent@*/ cstring - cstring_makeLiteralTemp (char *) /*@*/ ; + cstring_makeLiteralTemp (const char *) /*@*/ ; # define cstring_makeLiteral(s) (cstring_copy (cstring_fromChars (s))) # define cstring_makeLiteralTemp(s) (cstring_fromChars (s)) -extern cstring cstring_capitalize (cstring p_s) /*@*/ /*@requires maxSet(p_s) >= 0 @*/ ; -extern cstring cstring_capitalizeFree (/*@only@*/ cstring p_s) /*@modifies p_s@*/ /*@requires maxSet(p_s) >= 0 /\ maxRead(p_s) >= 0 @*/ ; +extern cstring cstring_capitalize (cstring p_s) + /*@*/ + /*@requires maxSet(p_s) >= 0 @*/ ; +extern cstring cstring_capitalizeFree (/*@only@*/ cstring p_s) + /*@modifies p_s@*/ + /*@requires maxSet(p_s) >= 0 /\ maxRead(p_s) >= 0 @*/ ; -extern cstring cstring_fill (cstring p_s, size_t p_n) /*@*/ /*@requires p_n >= 0 @*/; +extern cstring cstring_fill (cstring p_s, size_t p_n) + /*@*/ + /*@requires p_n >= 0 @*/; extern cstring cstring_prefix (cstring p_s, size_t p_n) /*@*/ @@ -153,7 +166,9 @@ extern cstring cstring_prefix (cstring p_s, size_t p_n) /*@ensures maxRead(result) == p_n /\ maxSet(result) == p_n @*/ ; extern /*@observer@*/ cstring cstring_suffix (cstring p_s, size_t p_n) /*@*/ ; -extern cstring cstring_concat (cstring p_s, cstring p_t) /*@*/ /*@requires maxSet(p_s) >= 0 @*/; +extern cstring cstring_concat (cstring p_s, cstring p_t) + /*@*/ + /*@requires maxSet(p_s) >= 0 @*/; extern cstring cstring_concatFree (/*@only@*/ cstring p_s, /*@only@*/ cstring p_t) @@ -164,7 +179,7 @@ extern cstring /*@modifies p_s@*/ ; extern cstring - cstring_concatChars (/*@only@*/ cstring p_s, char *p_t) + cstring_concatChars (/*@only@*/ cstring p_s, const char *p_t) /*@modifies p_s@*/ ; extern lsymbol cstring_toSymbol (/*@only@*/ cstring p_s) /*@*/ ; @@ -197,12 +212,12 @@ extern /*@notnull@*/ cstring cstring_expandEscapes (cstring p_s); extern size_t cstring_lengthExpandEscapes (cstring p_s); -extern bool cstring_containsLit (/*@unique@*/ cstring p_c, char *p_sub) /*@*/ ; +extern bool cstring_containsLit (/*@unique@*/ cstring p_c, const char *p_sub) /*@*/ ; # define cstring_containsLit(c,sub) \ (cstring_contains (c, cstring_fromChars (sub))) /*drl added July 2, 001 */ -extern int cstring_compareLit (/*@unique@*/ cstring p_c, char *p_sub) /*@*/ ; +extern int cstring_compareLit (/*@unique@*/ cstring p_c, const char *p_sub) /*@*/ ; # define cstring_compareLit(c,sub) \ (cstring_compare (c, cstring_fromChars (sub))) diff --git a/src/cstring.c b/src/cstring.c index 7098ab1..f4f7393 100644 --- a/src/cstring.c +++ b/src/cstring.c @@ -163,9 +163,10 @@ char cstring_lastChar (cstring s) } } -/*@only@*/ cstring cstring_copyLength (char *s, size_t len) /*@requires maxSet(s) >= (len - 1) @*/ +/*@only@*/ cstring +cstring_copyLength (const char *s, size_t len) /*@requires maxSet(s) >= (len - 1) @*/ { - char *res = mstring_create (len + 1); + char *res = mstring_create (len); strncpy (res, s, len); res[len] = '\0'; @@ -717,22 +718,37 @@ cstring_concatFree1 (cstring s, cstring t) } /*@only@*/ cstring -cstring_concatChars (cstring s, char *t) +cstring_concatChars (cstring s, const char *t) { - cstring res = cstring_concat (s, cstring_fromChars (t)); - cstring_free (s); - return res; + if (t != NULL) + { + return cstring_concatLength (s, t, strlen (t)); + } + + return s; } /*@only@*/ cstring -cstring_concatLength (cstring s1, char *s2, size_t len) /*@requires maxSet(s2) >= (len - 1) @*/ +cstring_concatLength (cstring s1, const char *s2, size_t len) /*@requires maxSet(s2) >= (len - 1) @*/ { - cstring tmp = cstring_copyLength (s2, len); - cstring res = cstring_concat (s1, tmp); - cstring_free (tmp); - cstring_free (s1); + if (len > 0) + { + char *res; + size_t s1len = cstring_length (s1); + + res = mstring_create (s1len + len); + if (cstring_isDefined (s1)) + { + strcpy (res, s1); + } + strncpy (res+s1len, s2, len); + res[s1len+len] = '\0'; + + cstring_free (s1); + return res; + } - return res; + return s1; } /*@only@*/ cstring -- 2.11.4.GIT