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.
This commit is contained in:
parent
05bc9ed9f0
commit
d16a91821d
|
@ -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
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -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
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue