C library: model inet_ntoa

Implement IPv4 inet_ntoa (translation from numeric addresses to a string
representation) by non-deterministically setting the byte string.

Author: tautschnig

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

@@ -0,0 +1,13 @@
+#ifndef _WIN32
+#  include <arpa/inet.h>
+#endif
+
+int main()
+{
+#ifndef _WIN32
+  struct in_addr input;
+  char *result = inet_ntoa(input);
+  (void)*result;
+#endif
+  return 0;
+}

regression/cbmc-library/inet_ntoa-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/inet.c

@@ -51,6 +51,28 @@ int inet_aton(const char *cp, struct in_addr *pin)
 
 #endif
 
+/* FUNCTION: inet_ntoa */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_INET_H_INCLUDED
+#    include <arpa/inet.h>
+#    define __CPROVER_INET_H_INCLUDED
+#  endif
+
+char __inet_ntoa_buffer[16];
+
+char *inet_ntoa(struct in_addr in)
+{
+__CPROVER_HIDE:;
+  (void)in;
+  // the last byte remains zero to ensure string termination
+  __CPROVER_havoc_slice(__inet_ntoa_buffer, 15);
+  return __inet_ntoa_buffer;
+}
+
+#endif
+
 /* FUNCTION: inet_network */
 
 #ifndef _WIN32