C library: Implement strcat, strncat

regression/cbmc/strcat1/main.c

@@ -0,0 +1,28 @@
+#include <string.h>
+#include <assert.h>
+
+int main()
+{
+  char A1[5] = {'a', 'b', '\0'};
+  char B1[3] = {'c', 'd', '\0'};
+
+  strcat(A1, B1);
+  assert(A1[3] == 'd');
+  assert(strlen(A1) == 4);
+
+  char A2[5] = {'a', 'b', '\0'};
+  char B2[3] = {'c', 'd', '\0'};
+
+  strncat(A2, B2, 2);
+  assert(A2[3] == 'd');
+  assert(strlen(A2) == 4);
+
+  char A3[5] = {'a', 'b', '\0'};
+  char B3[3] = {'c', 'd', '\0'};
+
+  strncat(A3, B3, 1);
+  assert(A3[3] == '\0');
+  assert(strlen(A3) == 4); // expected to fail
+
+  return 0;
+}

regression/cbmc/strcat1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwind 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.6\] assertion strlen\(A3\) == 4: FAILURE
+\*\* 1 of 8 failed
+--
+^warning: ignoring

src/ansi-c/library/string.c

@@ -52,15 +52,13 @@ __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size
   while(dst[i]!=0) i++;
 
   __CPROVER_size_t j=0;
-  char ch;
-  do
+  char ch = 1;
+  for(; i < s && ch != (char)0; ++i, ++j)
   {
     ch=src[j];
     dst[i]=ch;
-    i++;
-    j++;
   }
-  while(i<s && ch!=(char)0);
+  dst[i] = '\0';
   #endif
   return dst;
 }
@@ -90,10 +88,19 @@ __inline char *__builtin___strncat_chk(
   #else
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "strncat src/dst overlap");
-  (void)*dst;
-  (void)*src;
-  (void)n;
-  (void)s;
+
+  __CPROVER_size_t i = 0;
+  while(dst[i] != 0)
+    i++;
+
+  __CPROVER_size_t j = 0;
+  char ch = 1;
+  for(; i < s && j < n && ch != (char)0; ++i, ++j)
+  {
+    ch = src[j];
+    dst[i] = ch;
+  }
+  dst[i] = '\0';
   #endif
   return dst;
 }
@@ -236,15 +243,13 @@ inline char *strcat(char *dst, const char *src)
   while(dst[i]!=0) i++;
 
   __CPROVER_size_t j=0;
-  char ch;
-  do
+  char ch = 1;
+  for(; ch != (char)0; ++i, ++j)
   {
     ch=src[j];
     dst[i]=ch;
-    i++;
-    j++;
   }
-  while(ch!=(char)0);
+  dst[i] = '\0';
   #endif
   return dst;
 }
@@ -279,9 +284,19 @@ inline char *strncat(char *dst, const char *src, size_t n)
   #else
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "strncat src/dst overlap");
-  (void)*dst;
-  (void)*src;
-  (void)n;
+
+  __CPROVER_size_t i = 0;
+  while(dst[i] != 0)
+    i++;
+
+  __CPROVER_size_t j = 0;
+  char ch = 1;
+  for(; j < n && ch != (char)0; ++i, ++j)
+  {
+    ch = src[j];
+    dst[i] = ch;
+  }
+  dst[i] = '\0';
   #endif
   return dst;
 }