From 7d4984f3a038a1c3c5509c307b6edda2627cfc23 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Jan 2018 12:21:32 +0000
Subject: [PATCH] C library: Implement strcat, strncat

---
 regression/cbmc/strcat1/main.c    | 28 ++++++++++++++++++
 regression/cbmc/strcat1/test.desc | 10 +++++++
 src/ansi-c/library/string.c       | 49 ++++++++++++++++++++-----------
 3 files changed, 70 insertions(+), 17 deletions(-)
 create mode 100644 regression/cbmc/strcat1/main.c
 create mode 100644 regression/cbmc/strcat1/test.desc

diff --git a/regression/cbmc/strcat1/main.c b/regression/cbmc/strcat1/main.c
new file mode 100644
index 0000000000..c71b86323d
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/strcat1/test.desc b/regression/cbmc/strcat1/test.desc
new file mode 100644
index 0000000000..288b76e89c
--- /dev/null
+++ b/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
diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 87eecf42c3..79993831ad 100644
--- a/src/ansi-c/library/string.c
+++ b/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;
 }