Merge pull request #5848 from tautschnig/fix-strcat

C library/str(n)cat: do not write spurious 0 byte

Author: tautschnig

regression/cbmc-library/strcat-01/main.c

@@ -10,19 +10,5 @@ int main()
   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-library/strcat-01/test.desc

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

regression/cbmc-library/strncat-01/main.c

@@ -3,7 +3,19 @@
 
 int main()
 {
-  strncat();
-  assert(0);
+  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-library/strncat-01/test.desc

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

src/ansi-c/library/string.c

@@ -72,7 +72,6 @@ __CPROVER_HIDE:;
     ch = src[j];
     dst[i] = ch;
   }
-  dst[i] = '\0';
 #endif
   return dst;
 }
@@ -122,7 +121,8 @@ __CPROVER_HIDE:;
     ch = src[j];
     dst[i] = ch;
   }
-  dst[i] = '\0';
+  if(ch != (char)0)
+    dst[i] = '\0';
 #endif
   return dst;
 }
@@ -288,7 +288,6 @@ __CPROVER_HIDE:;
     ch = src[j];
     dst[i] = ch;
   }
-  dst[i] = '\0';
 #endif
   return dst;
 }
@@ -342,7 +341,8 @@ __CPROVER_HIDE:;
     ch = src[j];
     dst[i] = ch;
   }
-  dst[i] = '\0';
+  if(ch != (char)0)
+    dst[i] = '\0';
 #endif
   return dst;
 }