C library: network byteorder functions

On some systems htonl etc. are just macros (always true for big-endian systems,
where they are null macros; and also true on Mac OS). For others we to provide
the implementation. In all cases the full support for bswap* is necessary, and
that is now available as of the preceding commit.

Also fixes arpa/inet.h being unavailable on Windows/Visual Studio.

Author: tautschnig

regression/cbmc/inet_endian1/main.c

@@ -0,0 +1,23 @@
+#ifndef _WIN32
+#include <arpa/inet.h>
+#include <assert.h>
+
+int main()
+{
+  uint32_t l;
+  assert(l == ntohl(htonl(l)));
+
+  uint16_t s;
+  assert(s == ntohs(htons(s)));
+
+  return 0;
+}
+
+#else
+
+int main()
+{
+  return 0;
+}
+
+#endif

regression/cbmc/inet_endian1/test.desc

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

src/ansi-c/library/inet.c

@@ -1,6 +1,11 @@
 /* FUNCTION: inet_addr */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
 #include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
 
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
@@ -16,8 +21,17 @@ in_addr_t inet_addr(const char *cp)
   return result;
 }
 
+#endif
+
 /* FUNCTION: inet_aton */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
+#include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
+
 int __VERIFIER_nondet_int();
 
 int inet_aton(const char *cp, struct in_addr *pin)
@@ -33,8 +47,17 @@ int inet_aton(const char *cp, struct in_addr *pin)
   return result;
 }
 
+#endif
+
 /* FUNCTION: inet_network */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
+#include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
+
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
 in_addr_t inet_network(const char *cp)
@@ -48,3 +71,87 @@ in_addr_t inet_network(const char *cp)
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
 }
+
+#endif
+
+/* FUNCTION: htonl */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef htonl
+
+uint32_t __builtin_bswap32(uint32_t);
+
+uint32_t htonl(uint32_t hostlong)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap32(hostlong);
+#else
+  return hostlong;
+#endif
+}
+
+/* FUNCTION: htons */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef htons
+
+uint16_t __builtin_bswap16(uint16_t);
+
+uint16_t htons(uint16_t hostshort)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap16(hostshort);
+#else
+  return hostlong;
+#endif
+}
+
+
+/* FUNCTION: ntohl */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef ntohl
+
+uint32_t __builtin_bswap32(uint32_t);
+
+uint32_t ntohl(uint32_t netlong)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap32(netlong);
+#else
+  return netlong;
+#endif
+}
+
+
+/* FUNCTION: ntohs */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef ntohs
+
+uint16_t __builtin_bswap16(uint16_t);
+
+uint16_t ntohs(uint16_t netshort)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap16(netshort);
+#else
+  return netshort;
+#endif
+}