Fixed problem with identifyFlag revealed by splint -help flags full

[splint.git] / src / cstring.c

diff --git a/src/cstring.c b/src/cstring.c
index 5213e341862be87a4bd9a0e99385df444a6ee789..fed415514c09be13da8f0d8615b6ba9f9fd3cdc5 100644 (file)
--- a/src/cstring.c
+++ b/src/cstring.c
@@ -212,11 +212,11 @@ void cstring_replaceAll (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) @*/
+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);
@@ -225,12 +225,15 @@ void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) /*@requi
        {
          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')