[Libc] clarification about strlcpy; fix spec of strndup

share/libc/string.h

@@ -372,7 +372,9 @@ extern char *strcpy(char *restrict dest, const char *restrict src);
 extern char *strncpy(char *restrict dest,
 		     const char *restrict src, size_t n);
 
-/*@ // Non-POSIX, but often present
+/*@ // Non-POSIX, but often present; note that, unlike strncpy, this has no
+  @ // "official specification" other than manpages. They state that src is
+  @ // a *string*, therefore its precondition is stricter than that of strncpy.
   @ requires valid_string_src: valid_read_string(src);
   @ requires room_nstring: \valid(dest+(0..n-1));
   @ requires separation:
@@ -475,7 +477,8 @@ extern size_t strxfrm (char *restrict dest,
   @*/
 extern char *strdup (const char *s);
 
-/*@ allocates \result;
+/*@ requires valid_string_s: valid_read_string(s);
+  @ allocates \result;
   @ assigns \result \from indirect:s[0..strlen(s)], indirect:n,
   @                       indirect:__fc_heap_status;
   @ behavior allocation:

tests/libc/string_h.c

@@ -120,6 +120,20 @@ void test_strncpy() {
   }
 }
 
+void test_strlcpy() {
+  char buf[16];
+  char buf2[32];
+  size_t r1 = strlcpy(buf, "longer than buffer", 16);
+  size_t r2 = strlcpy(buf2, "short", 16);
+  size_t r3 = strlcat(buf2, buf, 32);
+  char src[] = { 'a', 'b', 'c' };
+  char dst[3];
+  if (nondet) {
+    strlcpy(dst,src,3);
+    //@ assert unreachable: \false;
+  }
+}
+
 int main(int argc, char **argv)
 {
   test_strcmp();
@@ -131,13 +145,9 @@ int main(int argc, char **argv)
   test_strtok_r();
   char *a = strdup("bla"); // unsound; specification currently unsupported
   char *b = strndup("bla", 2); // unsound; specification currently unsupported
-  char buf[16];
-  char buf2[32];
-  size_t r1 = strlcpy(buf, "longer than buffer", 16);
-  size_t r2 = strlcpy(buf2, "short", 16);
-  size_t r3 = strlcat(buf2, buf, 32);
   char *strsig = strsignal(1);
   //@ assert valid_read_string(strsig);
   test_strncpy();
+  test_strlcpy();
   return 0;
 }