diff --git a/regression/cbmc/memcpy1/main.c b/regression/cbmc/memcpy1/main.c
new file mode 100644
index 00000000000..2c2d2495035
--- /dev/null
+++ b/regression/cbmc/memcpy1/main.c
@@ -0,0 +1,12 @@
+#include <stdint.h>
+#include <string.h>
+
+int main()
+{
+  uint8_t a;
+  uint32_t b;
+
+  memcpy(&b, &a, sizeof(b));
+
+  return 0;
+}
diff --git a/regression/cbmc/memcpy1/test.desc b/regression/cbmc/memcpy1/test.desc
new file mode 100644
index 00000000000..87a13eb5452
--- /dev/null
+++ b/regression/cbmc/memcpy1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.16\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed long (long )?int\)n\) - \(signed long (long )?int\)1\): FAILURE$
+\*\* 1 of 17 failed
+--
+^warning: ignoring
diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc
index 0c1bb9e7ab4..9cb43afa709 100644
--- a/regression/cbmc/memset3/test.desc
+++ b/regression/cbmc/memset3/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
-\*\* 1 of .* failed \(.*\)
+\*\* 2 of .* failed \(.*\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc/strcat1/main.c b/regression/cbmc/strcat1/main.c
new file mode 100644
index 00000000000..c71b86323de
--- /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 00000000000..288b76e89cb
--- /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 87eecf42c31..b1101f22248 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;
 }
@@ -533,10 +548,16 @@ void *memcpy(void *dst, const void *src, size_t n)
                    __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
   (void)*(char *)dst; // check that the memory is accessible
   (void)*(const char *)src; // check that the memory is accessible
-  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
-  char src_n[n];
-  __CPROVER_array_copy(src_n, (char*)src);
-  __CPROVER_array_replace((char*)dst, src_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)dst) + n - 1);       // check that the memory is accessible
+    (void)*(((const char *)src) + n - 1); // check that the memory is accessible
+    //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+    char src_n[n];
+    __CPROVER_array_copy(src_n, (char *)src);
+    __CPROVER_array_replace((char *)dst, src_n);
+  }
   #endif
   return dst;
 }
@@ -566,10 +587,16 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
   (void)*(char *)dst; // check that the memory is accessible
   (void)*(const char *)src; // check that the memory is accessible
   (void)size;
-  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
-  char src_n[n];
-  __CPROVER_array_copy(src_n, (char*)src);
-  __CPROVER_array_replace((char*)dst, src_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)dst) + n - 1);       // check that the memory is accessible
+    (void)*(((const char *)src) + n - 1); // check that the memory is accessible
+    //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+    char src_n[n];
+    __CPROVER_array_copy(src_n, (char *)src);
+    __CPROVER_array_replace((char *)dst, src_n);
+  }
   #endif
   return dst;
 }
@@ -603,11 +630,16 @@ void *memset(void *s, int c, size_t n)
     __CPROVER_is_zero_string(s)=0;
   #else
   (void)*(char *)s; // check that the memory is accessible
-  //char *sp=s;
-  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
-  unsigned char s_n[n];
-  __CPROVER_array_set(s_n, (unsigned char)c);
-  __CPROVER_array_replace((unsigned char*)s, s_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)s) + n - 1); // check that the memory is accessible
+    //char *sp=s;
+    //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+    unsigned char s_n[n];
+    __CPROVER_array_set(s_n, (unsigned char)c);
+    __CPROVER_array_replace((unsigned char *)s, s_n);
+  }
   #endif
   return s;
 }
@@ -631,13 +663,21 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
     __CPROVER_zero_string_length(s)=0;
   }
   else
+  {
     __CPROVER_is_zero_string(s)=0;
+  }
   #else
-  //char *sp=s;
-  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
-  unsigned char s_n[n];
-  __CPROVER_array_set(s_n, (unsigned char)c);
-  __CPROVER_array_replace((unsigned char*)s, s_n);
+  (void)*(char *)s; // check that the memory is accessible
+
+  if(n > 0)
+  {
+    (void)*(((char *)s) + n - 1); // check that the memory is accessible
+    //char *sp=s;
+    //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+    unsigned char s_n[n];
+    __CPROVER_array_set(s_n, (unsigned char)c);
+    __CPROVER_array_replace((unsigned char *)s, s_n);
+  }
   #endif
   return s;
 }
@@ -666,11 +706,16 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
   #else
   (void)*(char *)s; // check that the memory is accessible
   (void)size;
-  //char *sp=s;
-  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
-  unsigned char s_n[n];
-  __CPROVER_array_set(s_n, (unsigned char)c);
-  __CPROVER_array_replace((unsigned char*)s, s_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)s) + n - 1); // check that the memory is accessible
+    //char *sp=s;
+    //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+    unsigned char s_n[n];
+    __CPROVER_array_set(s_n, (unsigned char)c);
+    __CPROVER_array_replace((unsigned char *)s, s_n);
+  }
   #endif
   return s;
 }
@@ -701,9 +746,15 @@ void *memmove(void *dest, const void *src, size_t n)
   #else
   (void)*(char *)dest; // check that the memory is accessible
   (void)*(const char *)src;  // check that the memory is accessible
-  char src_n[n];
-  __CPROVER_array_copy(src_n, (char*)src);
-  __CPROVER_array_replace((char*)dest, src_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)dest) + n - 1);      // check that the memory is accessible
+    (void)*(((const char *)src) + n - 1); // check that the memory is accessible
+    char src_n[n];
+    __CPROVER_array_copy(src_n, (char *)src);
+    __CPROVER_array_replace((char *)dest, src_n);
+  }
   #endif
   return dest;
 }
@@ -731,12 +782,22 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
     __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
   }
   else
+  {
     __CPROVER_is_zero_string(dest)=0;
+  }
   #else
+  (void)*(char *)dest; // check that the memory is accessible
+  (void)*(const char *)src;  // check that the memory is accessible
   (void)size;
-  char src_n[n];
-  __CPROVER_array_copy(src_n, (char*)src);
-  __CPROVER_array_replace((char*)dest, src_n);
+
+  if(n > 0)
+  {
+    (void)*(((char *)dest) + n - 1);      // check that the memory is accessible
+    (void)*(((const char *)src) + n - 1); // check that the memory is accessible
+    char src_n[n];
+    __CPROVER_array_copy(src_n, (char *)src);
+    __CPROVER_array_replace((char *)dest, src_n);
+  }
   #endif
   return dest;
 }