diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index eb57e0efbaa5ee79c9810fe091b10d253e9c868d..0dec616323d28ea20e2712e5d8c5d6b2657fa54e 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -344,7 +344,22 @@ extern int     bind(int sockfd, const struct sockaddr *addr, socklen_t addrlen);
 extern int connect(int sockfd, const struct sockaddr *addr, socklen_t addrlen);
 
 extern int     getpeername(int, struct sockaddr *, socklen_t *);
-extern int     getsockname(int, struct sockaddr *, socklen_t *);
+
+/*@
+  // missing: may assign to errno: EBADF, ENOTSOCK, EOPNOTSUPP, EINVAL, ENOBUFS
+  requires valid_sockfd: 0 <= socket < __FC_MAX_OPEN_SOCKETS;
+  requires valid_address_len: \valid(address_len);
+  requires initialization:address_len: \initialized(address_len);
+  requires valid_address: \valid(((char*)address)+(0 .. *address_len-1));
+  assigns *address_len \from indirect:socket, __fc_sockfds[socket];
+  assigns \result \from indirect:__fc_sockfds[socket], indirect:socket;
+  assigns ((char*)address)[0 .. (*address_len)-1] \from
+          indirect:__fc_sockfds[socket], indirect:socket;
+  ensures new_address_len: *address_len <= \old(*address_len);
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int getsockname(int socket, struct sockaddr *restrict address,
+                       socklen_t *restrict address_len);
 
 // getsockopt is incrementally specified: options which are used more often
 // are gradually refined; the rest are handled by behavior "other_options".
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 4dec6771dc9a74dde8972587bb342d35956a8b6b..d64b91d8754bfeb84252812247ac698571ba6433 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
    unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
    wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
   
-  Undefined functions (384)
+  Undefined functions (385)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -100,25 +100,26 @@
    getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
    getpwuid (0 call); getresgid (0 call); getresuid (0 call);
    getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
-   getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
-   gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
-   iconv_close (0 call); iconv_open (0 call); inet_addr (2 calls);
-   inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
-   isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
-   killpg (0 call); labs (0 call); lcong48 (0 call); ldiv (0 call);
-   listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
-   log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
-   log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
-   longjmp (0 call); lrand48 (0 call); lseek (0 call); malloc (7 calls);
-   mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
-   mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
-   nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
-   ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
-   opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
-   perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
-   powf (0 call); pthread_cond_broadcast (0 call);
-   pthread_cond_destroy (0 call); pthread_cond_init (0 call);
-   pthread_cond_wait (0 call); pthread_create (0 call); pthread_join (0 call);
+   getsockname (0 call); getsockopt (0 call); gettimeofday (0 call);
+   getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
+   iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+   inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
+   inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
+   kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
+   ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
+   localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
+   log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
+   logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
+   lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
+   mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
+   mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
+   nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
+   open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
+   pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+   poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+   pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
+   pthread_cond_init (0 call); pthread_cond_wait (0 call);
+   pthread_create (0 call); pthread_join (0 call);
    pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
    pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
    putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -178,7 +179,7 @@
   Goto = 89
   Assignment = 438
   Exit point = 82
-  Function = 466
+  Function = 467
   Function call = 89
   Pointer dereferencing = 158
   Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index cca33149a94ff6a98e03d64c5f95b6ffb602f4d0..e416b9691aac6d79361d25a812da9f4d4502470c 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3667,6 +3667,24 @@ extern int bind(int sockfd, struct sockaddr const *addr, socklen_t addrlen);
  */
 extern int connect(int sockfd, struct sockaddr const *addr, socklen_t addrlen);
 
+/*@ requires valid_sockfd: 0 ≤ socket < 1024;
+    requires valid_address_len: \valid(address_len);
+    requires initialization: address_len: \initialized(address_len);
+    requires
+      valid_address: \valid((char *)address + (0 .. *address_len - 1));
+    ensures new_address_len: *\old(address_len) ≤ \old(*address_len);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns *address_len, \result,
+            *((char *)address + (0 .. *address_len - 1));
+    assigns *address_len \from (indirect: socket), __fc_sockfds[socket];
+    assigns \result
+      \from (indirect: __fc_sockfds[socket]), (indirect: socket);
+    assigns *((char *)address + (0 .. *address_len - 1))
+      \from (indirect: __fc_sockfds[socket]), (indirect: socket);
+ */
+extern int getsockname(int socket, struct sockaddr * __restrict address,
+                       socklen_t * __restrict address_len);
+
 /*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
     requires valid_optlen: \valid(optlen);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
diff --git a/tests/libc/oracle/socket_h.res.oracle b/tests/libc/oracle/socket_h.res.oracle
index 58758f9d5654c9a66fe52f39c0e0bd6c4c2dcd83..fb67e21c1df1632acbdfaed561ee56229063ce04 100644
--- a/tests/libc/oracle/socket_h.res.oracle
+++ b/tests/libc/oracle/socket_h.res.oracle
@@ -3,7 +3,7 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
+  v ∈ [--..--]
 [eva] computing for function socket <- main.
   Called from tests/libc/socket_h.c:7.
 [eva] using specification for function socket
@@ -47,6 +47,18 @@
 [eva] tests/libc/socket_h.c:18: 
   function getsockopt, behavior so_error: precondition 'valid_optval' got status valid.
 [eva] Done for function getsockopt
+[eva] computing for function getsockname <- main.
+  Called from tests/libc/socket_h.c:21.
+[eva] using specification for function getsockname
+[eva] tests/libc/socket_h.c:21: 
+  function getsockname: precondition 'valid_sockfd' got status valid.
+[eva] tests/libc/socket_h.c:21: 
+  function getsockname: precondition 'valid_address_len' got status valid.
+[eva] tests/libc/socket_h.c:21: 
+  function getsockname: precondition 'initialization,address_len' got status valid.
+[eva] tests/libc/socket_h.c:21: 
+  function getsockname: precondition 'valid_address' got status valid.
+[eva] Done for function getsockname
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -59,3 +71,5 @@
   rc ∈ {-1; 0}
   optval ∈ [--..--] or UNINITIALIZED
   optlen ∈ {4}
+  addr2 ∈ [--..--] or UNINITIALIZED
+  socklen ∈ [0..8]
diff --git a/tests/libc/socket_h.c b/tests/libc/socket_h.c
index 8254f9250c808926539bc9179de001598468a4f8..3a0e8d8cab974f29eb249f53759997d661e740d1 100644
--- a/tests/libc/socket_h.c
+++ b/tests/libc/socket_h.c
@@ -2,7 +2,7 @@
 #include <sys/types.h>
 #include <sys/socket.h>
 #include <stdlib.h>
-
+volatile int v;
 int main() {
   int sockfd = socket(AF_INET, SOCK_STREAM, 0);
   if (sockfd < 0) exit(1);
@@ -16,5 +16,8 @@ int main() {
   int optval;
   socklen_t optlen = sizeof(optval);
   rc = getsockopt(sockfd, SOL_SOCKET, SO_ERROR, (void *)&optval, &optlen);
+  struct sockaddr_in addr2;
+  socklen_t socklen = sizeof(addr2);
+  rc = getsockname(sockfd, (struct sockaddr *)&addr2, &socklen);
   return rc;
 }