Mostly tasteful/consistent splint annotations for libelf.

CVS patchset: 5827
CVS date: 2002/11/05 23:00:34

87 files changed, 502 insertions, 423 deletions

diff --git a/elfutils/libelf/common.h b/elfutils/libelf/common.h
index fc5ccd2aa..249cc11ba 100644
--- a/elfutils/libelf/common.h
+++ b/elfutils/libelf/common.h
@@ -27,6 +27,7 @@
 
 static inline Elf_Kind
 determine_kind (void *buf, size_t len)
+	/*@*/
 {
   /* First test for an archive.  */
   if (len >= SARMAG && memcmp (buf, ARMAG, SARMAG) == 0)
@@ -52,9 +53,12 @@ determine_kind (void *buf, size_t len)
 
 
 /* Allocate an Elf descriptor and fill in the generic information.  */
+/*@null@*/
 static inline Elf *
-allocate_elf (int fildes, void *map_address, off_t offset, size_t maxsize,
-              Elf_Cmd cmd, Elf *parent, Elf_Kind kind, size_t extra)
+allocate_elf (int fildes, /*@null@*/ void *map_address, off_t offset,
+	      size_t maxsize, Elf_Cmd cmd, /*@null@*/ Elf *parent,
+	      Elf_Kind kind, size_t extra)
+	/*@*/
 {
   Elf *result = (Elf *) calloc (1, sizeof (Elf) + extra);
   if (result == NULL)
@@ -80,6 +84,7 @@ allocate_elf (int fildes, void *map_address, off_t offset, size_t maxsize,
 /* Acquire lock for the descriptor and all children.  */
 static void
 libelf_acquire_all (Elf *elf)
+	/*@modifies elf @*/
 {
   rwlock_wrlock (elf->lock);
 
@@ -99,6 +104,7 @@ libelf_acquire_all (Elf *elf)
 /* Release own lock and those of the children.  */
 static void
 libelf_release_all (Elf *elf)
+	/*@modifies elf @*/
 {
   if (elf->kind == ELF_K_AR)
     {
diff --git a/elfutils/libelf/crc32.c b/elfutils/libelf/crc32.c
index a415013d2..ca2255051 100644
--- a/elfutils/libelf/crc32.c
+++ b/elfutils/libelf/crc32.c
@@ -23,6 +23,7 @@
 #include <sys/types.h>
 
 /* Table computed with Mark Adler's makecrc.c utility.  */
+/*@unchecked@*/
 static const uint32_t crc32_table[256] =
 {
   0x00000000, 0x77073096, 0xee0e612c, 0x990951ba, 0x076dc419,
diff --git a/elfutils/libelf/dl-hash.h b/elfutils/libelf/dl-hash.h
index 1e943afc5..471f84f1e 100644
--- a/elfutils/libelf/dl-hash.h
+++ b/elfutils/libelf/dl-hash.h
@@ -25,6 +25,7 @@
 static inline unsigned int
 __attribute__ ((__pure__))
 _dl_elf_hash (const char *name)
+	/*@*/
 {
   unsigned int hash = (unsigned int) *((const unsigned char *) name)++;
   if (*name != '\0')
diff --git a/elfutils/libelf/elf32_fsize.c b/elfutils/libelf/elf32_fsize.c
index 52b5af942..b37475283 100644
--- a/elfutils/libelf/elf32_fsize.c
+++ b/elfutils/libelf/elf32_fsize.c
@@ -28,10 +28,7 @@
 
 
 size_t
-elfw2(LIBELFBITS, fsize) (type, count, version)
-     Elf_Type type;
-     size_t count;
-     unsigned int version;
+elfw2(LIBELFBITS, fsize) (Elf_Type type, size_t count, unsigned int version)
 {
   /* We do not have differences between file and memory sizes.  Better
      not since otherwise `mmap' would not work.  */
@@ -55,5 +52,8 @@ elfw2(LIBELFBITS, fsize) (type, count, version)
 	  * __libelf_type_sizes[0][ELFW(ELFCLASS,LIBELFBITS) - 1][type]);
 #endif
 }
+
+#if !defined(__LCLINT__)
 #define local_strong_alias(n1, n2) strong_alias (n1, n2)
 local_strong_alias (elfw2(LIBELFBITS, fsize), __elfw2(LIBELFBITS, msize))
+#endif
diff --git a/elfutils/libelf/elf32_getehdr.c b/elfutils/libelf/elf32_getehdr.c
index 282d06220..e29d9d1ec 100644
--- a/elfutils/libelf/elf32_getehdr.c
+++ b/elfutils/libelf/elf32_getehdr.c
@@ -30,8 +30,7 @@
 
 
 ElfW2(LIBELFBITS,Ehdr) *
-elfw2(LIBELFBITS,getehdr) (elf)
-     Elf *elf;
+elfw2(LIBELFBITS,getehdr) (Elf *elf)
 {
   ElfW2(LIBELFBITS,Ehdr) *result;
 
diff --git a/elfutils/libelf/elf32_getphdr.c b/elfutils/libelf/elf32_getphdr.c
index d224fad16..0ac3076a9 100644
--- a/elfutils/libelf/elf32_getphdr.c
+++ b/elfutils/libelf/elf32_getphdr.c
@@ -34,8 +34,7 @@
 #endif
 
 ElfW2(LIBELFBITS,Phdr) *
-elfw2(LIBELFBITS,getphdr) (elf)
-     Elf *elf;
+elfw2(LIBELFBITS,getphdr) (Elf *elf)
 {
   ElfW2(LIBELFBITS,Phdr) *result;
 
diff --git a/elfutils/libelf/elf32_getshdr.c b/elfutils/libelf/elf32_getshdr.c
index e5fc7f190..fd5ab3e55 100644
--- a/elfutils/libelf/elf32_getshdr.c
+++ b/elfutils/libelf/elf32_getshdr.c
@@ -34,8 +34,7 @@
 #endif
 
 ElfW2(LIBELFBITS,Shdr) *
-elfw2(LIBELFBITS,getshdr) (scn)
-     Elf_Scn *scn;
+elfw2(LIBELFBITS,getshdr) (Elf_Scn *scn)
 {
   ElfW2(LIBELFBITS,Shdr) *result;
 
diff --git a/elfutils/libelf/elf32_newehdr.c b/elfutils/libelf/elf32_newehdr.c
index 47e814477..c712d0406 100644
--- a/elfutils/libelf/elf32_newehdr.c
+++ b/elfutils/libelf/elf32_newehdr.c
@@ -30,8 +30,7 @@
 
 
 ElfW2(LIBELFBITS,Ehdr) *
-elfw2(LIBELFBITS,newehdr) (elf)
-     Elf *elf;
+elfw2(LIBELFBITS,newehdr) (Elf *elf)
 {
   ElfW2(LIBELFBITS,Ehdr) *result;
 
diff --git a/elfutils/libelf/elf32_newphdr.c b/elfutils/libelf/elf32_newphdr.c
index 2a98f2962..05aa7a17a 100644
--- a/elfutils/libelf/elf32_newphdr.c
+++ b/elfutils/libelf/elf32_newphdr.c
@@ -31,9 +31,7 @@
 
 
 ElfW2(LIBELFBITS,Phdr) *
-elfw2(LIBELFBITS,newphdr) (elf, count)
-     Elf *elf;
-     size_t count;
+elfw2(LIBELFBITS,newphdr) (Elf *elf, size_t count)
 {
   ElfW2(LIBELFBITS,Phdr) *result;
 
diff --git a/elfutils/libelf/elf32_updatefile.c b/elfutils/libelf/elf32_updatefile.c
index 6495db03b..36b3f0d13 100644
--- a/elfutils/libelf/elf32_updatefile.c
+++ b/elfutils/libelf/elf32_updatefile.c
@@ -261,6 +261,7 @@ __elfw2(LIBELFBITS,updatemmap) (Elf *elf, int change_bo, size_t shnum)
 /* Helper function to write out fill bytes.  */
 static int
 fill (int fd, off_t pos, size_t len, char *fillbuf, size_t *filledp)
+	/*@modifies fillbuf, filledp @*/
 {
   size_t filled = *filledp;
 
diff --git a/elfutils/libelf/elf32_updatenull.c b/elfutils/libelf/elf32_updatenull.c
index 4820d0bbf..95ec31a73 100644
--- a/elfutils/libelf/elf32_updatenull.c
+++ b/elfutils/libelf/elf32_updatenull.c
@@ -37,6 +37,7 @@
 static int
 ELFW(default_ehdr,LIBELFBITS) (Elf *elf, ElfW2(LIBELFBITS,Ehdr) *ehdr,
 			       size_t shnum, int *change_bop)
+	/*@modifies elf, ehdr, *change_bop @*/
 {
   /* Always write the magic bytes.  */
   if (memcmp (&ehdr->e_ident[EI_MAG0], ELFMAG, SELFMAG) != 0)
@@ -177,7 +178,7 @@ __elfw2(LIBELFBITS,updatenull) (Elf *elf, int *change_bop, size_t shnum)
 
 	      assert (shdr != NULL);
 	      sh_entsize = shdr->sh_entsize;
-	      sh_align = shdr->sh_addralign ?: 1;
+	      sh_align = shdr->sh_addralign ? shdr->sh_addralign : 1;
 
 	      /* Set the sh_entsize value if we can reliably detect it.  */
 	      switch (shdr->sh_type)
diff --git a/elfutils/libelf/elf32_xlatetof.c b/elfutils/libelf/elf32_xlatetof.c
index 501f41cdd..9128dd2f5 100644
--- a/elfutils/libelf/elf32_xlatetof.c
+++ b/elfutils/libelf/elf32_xlatetof.c
@@ -31,10 +31,8 @@
 
 
 Elf_Data *
-elfw2(LIBELFBITS, xlatetof) (dest, src, encode)
-     Elf_Data *dest;
-     const Elf_Data *src;
-     unsigned int encode;
+elfw2(LIBELFBITS, xlatetof) (Elf_Data *dest, const Elf_Data *src,
+			     unsigned int encode)
 {
   /* First test whether the input data is really suitable for this
      type.  This means, whether there is an integer number of records.
diff --git a/elfutils/libelf/elf32_xlatetom.c b/elfutils/libelf/elf32_xlatetom.c
index f70b5dfb7..953a9f28f 100644
--- a/elfutils/libelf/elf32_xlatetom.c
+++ b/elfutils/libelf/elf32_xlatetom.c
@@ -31,10 +31,8 @@
 
 
 Elf_Data *
-elfw2(LIBELFBITS, xlatetom) (dest, src, encode)
-     Elf_Data *dest;
-     const Elf_Data *src;
-     unsigned int encode;
+elfw2(LIBELFBITS, xlatetom) (Elf_Data *dest, const Elf_Data *src,
+			     unsigned int encode)
 {
   /* First test whether the input data is really suitable for this
      type.  This means, whether there is an integer number of records.
diff --git a/elfutils/libelf/elf_begin.c b/elfutils/libelf/elf_begin.c
index 0976b6fc3..21a4e1f6d 100644
--- a/elfutils/libelf/elf_begin.c
+++ b/elfutils/libelf/elf_begin.c
@@ -37,9 +37,11 @@
 #endif
 
 /* Create descriptor for archive in memory.  */
+/*@null@*/
 static inline Elf *
-file_read_ar (int fildes, void *map_address, off_t offset, size_t maxsize,
-	      Elf_Cmd cmd, Elf *parent)
+file_read_ar (int fildes, /*@null@*/ void *map_address, off_t offset,
+	      size_t maxsize, Elf_Cmd cmd, /*@null@*/ Elf *parent)
+	/*@*/
 {
   Elf *elf;
 
@@ -60,8 +62,9 @@ file_read_ar (int fildes, void *map_address, off_t offset, size_t maxsize,
 
 
 static size_t
-get_shnum (void *map_address, unsigned char *e_ident, int fildes, off_t offset,
-	   size_t maxsize)
+get_shnum (/*@null@*/ void *map_address, unsigned char *e_ident, int fildes,
+	   off_t offset, size_t maxsize)
+	/*@*/
 {
   size_t result;
   union
@@ -177,9 +180,11 @@ get_shnum (void *map_address, unsigned char *e_ident, int fildes, off_t offset,
 
 
 /* Create descriptor for ELF file in memory.  */
+/*@null@*/
 static Elf *
-file_read_elf (int fildes, void *map_address, off_t offset, size_t maxsize,
-	       Elf_Cmd cmd, Elf *parent)
+file_read_elf (int fildes, /*@null@*/ void *map_address, off_t offset, size_t maxsize,
+	       Elf_Cmd cmd, /*@null@*/ Elf *parent)
+	/*@*/
 {
   /* We only read the ELF header now.  */
   unsigned char *e_ident;
@@ -436,9 +441,11 @@ __libelf_read_mmaped_file (int fildes, void *map_address,  off_t offset,
 }
 
 
+/*@null@*/
 static Elf *
 read_unmmaped_file (int fildes, off_t offset, size_t maxsize, Elf_Cmd cmd,
-		    Elf *parent)
+		    /*@null@*/ Elf *parent)
+	/*@*/
 {
   /* We have to find out what kind of file this is.  We handle ELF
      files and archives.  To find out what we have we must read the
@@ -486,9 +493,11 @@ read_unmmaped_file (int fildes, off_t offset, size_t maxsize, Elf_Cmd cmd,
 
 
 /* Open a file for reading.  If possible we will try to mmap() the file.  */
+/*@null@*/
 static struct Elf *
 read_file (int fildes, off_t offset, size_t maxsize,
 	   Elf_Cmd cmd, Elf *parent)
+	/*@*/
 {
   void *map_address = NULL;
   int use_mmap = (cmd == ELF_C_READ_MMAP || cmd == ELF_C_RDWR_MMAP
@@ -559,8 +568,10 @@ read_file (int fildes, off_t offset, size_t maxsize,
 
 
 /* Find the entry with the long names for the content of this archive.  */
+/*@null@*/
 static const char *
 read_long_names (Elf *elf)
+	/*@modifies elf @*/
 {
   off_t offset = SARMAG;	/* This is the first entry.  */
   struct ar_hdr hdrm;
@@ -655,8 +666,7 @@ read_long_names (Elf *elf)
 /* Read the next archive header.  */
 int
 internal_function
-__libelf_next_arhdr (elf)
-     Elf *elf;
+__libelf_next_arhdr (Elf *elf)
 {
   struct ar_hdr *ar_hdr;
   Elf_Arhdr *elf_ar_hdr;
@@ -872,8 +882,10 @@ __libelf_next_arhdr (elf)
 /* We were asked to return a clone of an existing descriptor.  This
    function must be called with the lock on the parent descriptor
    being held. */
+/*@null@*/
 static Elf *
 dup_elf (int fildes, Elf_Cmd cmd, Elf *ref)
+	/*@modifies ref @*/
 {
   struct Elf *result;
 
@@ -935,8 +947,10 @@ dup_elf (int fildes, Elf_Cmd cmd, Elf *ref)
 
 
 /* Return desriptor for empty file ready for writing.  */
+/*@null@*/
 static struct Elf *
 write_file (int fd, Elf_Cmd cmd)
+	/*@*/
 {
   /* We simply create an empty `Elf' structure.  */
 #define NSCNSALLOC	10
@@ -964,10 +978,7 @@ write_file (int fd, Elf_Cmd cmd)
 
 /* Return a descriptor for the file belonging to FILDES.  */
 Elf *
-elf_begin (fildes, cmd, ref)
-     int fildes;
-     Elf_Cmd cmd;
-     Elf *ref;
+elf_begin (int fildes, Elf_Cmd cmd, Elf *ref)
 {
   Elf *retval;
 
diff --git a/elfutils/libelf/elf_cntl.c b/elfutils/libelf/elf_cntl.c
index 0225f81fd..cf8616783 100644
--- a/elfutils/libelf/elf_cntl.c
+++ b/elfutils/libelf/elf_cntl.c
@@ -25,9 +25,7 @@
 
 
 int
-elf_cntl (elf, cmd)
-     Elf *elf;
-     Elf_Cmd cmd;
+elf_cntl (Elf *elf, Elf_Cmd cmd)
 {
   int result = 0;
 
diff --git a/elfutils/libelf/elf_end.c b/elfutils/libelf/elf_end.c
index 7dd9d7905..424b4deba 100644
--- a/elfutils/libelf/elf_end.c
+++ b/elfutils/libelf/elf_end.c
@@ -28,8 +28,7 @@
 
 
 int
-elf_end (elf)
-     Elf *elf;
+elf_end (Elf *elf)
 {
   Elf *parent;
 
diff --git a/elfutils/libelf/elf_error.c b/elfutils/libelf/elf_error.c
index 9cd41e869..0361f9d20 100644
--- a/elfutils/libelf/elf_error.c
+++ b/elfutils/libelf/elf_error.c
@@ -29,19 +29,28 @@
 
 
 /* This is the key for the thread specific memory.  */
+/*@unchecked@*/ /*@null@*/
 static tls_key_t key;
 
 /* The error number.  Used in non-threaded programs.  */
+/*@unchecked@*/
 static int global_error;
+/*@unchecked@*/
 static bool threaded;
 /* We need to initialize the thread-specific data.  */
+/*@unchecked@*/
 once_define (static, once);
 
 /* The initialization and destruction functions.  */
-static void init (void);
-static void free_key_mem (void *mem);
+static void init (void)
+	/*@globals threaded @*/
+	/*@modifies threaded @*/;
+static void free_key_mem (void *mem)
+	/*@globals key @*/
+	/*@modifies key @*/;
 
 
+/*@-mods@*/
 int
 elf_errno (void)
 {
@@ -64,11 +73,13 @@ elf_errno (void)
   global_error = ELF_E_NOERROR;
   return result;
 }
+/*@=mods@*/
 
 
+/*@-mods@*/
 void
-__libelf_seterrno (value)
-     int value;
+internal_function
+__libelf_seterrno (int value)
 {
   /* If we have not yet initialized the buffer do it now.  */
   once_execute (once, init);
@@ -80,9 +91,11 @@ __libelf_seterrno (value)
 
   global_error = value;
 }
+/*@=mods@*/
 
 
 /* Return the appropriate message for the error.  */
+/*@unchecked@*/
 static const char msgstr[] =
 {
 #define ELF_E_NOERROR_IDX 0
@@ -246,6 +259,7 @@ static const char msgstr[] =
 };
 
 
+/*@unchecked@*/
 static const uint_fast16_t msgidx[ELF_E_NUM] =
 {
   [ELF_E_NOERROR] = ELF_E_NOERROR_IDX,
@@ -291,9 +305,9 @@ static const uint_fast16_t msgidx[ELF_E_NUM] =
 };
 
 
+/*@-mods@*/
 const char *
-elf_errmsg (error)
-     int error;
+elf_errmsg (int error)
 {
   int last_error;
 
@@ -318,6 +332,7 @@ elf_errmsg (error)
   assert (msgidx[error == -1 ? last_error : error] < sizeof (msgstr));
   return _(msgstr + msgidx[error == -1 ? last_error : error]);
 }
+/*@=mods@*/
 
 
 /* Free the thread specific data, this is done if a thread terminates.  */
diff --git a/elfutils/libelf/elf_fill.c b/elfutils/libelf/elf_fill.c
index 8b1d14a5b..307646567 100644
--- a/elfutils/libelf/elf_fill.c
+++ b/elfutils/libelf/elf_fill.c
@@ -27,9 +27,10 @@
 int __libelf_fill_byte;
 
 
+/*@-mods@*/
 void
-elf_fill (fill)
-     int fill;
+elf_fill (int fill)
 {
   __libelf_fill_byte = fill;
 }
+/*@=mods@*/
diff --git a/elfutils/libelf/elf_flagdata.c b/elfutils/libelf/elf_flagdata.c
index 1927bceb4..b967eac09 100644
--- a/elfutils/libelf/elf_flagdata.c
+++ b/elfutils/libelf/elf_flagdata.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagdata (data, cmd, flags)
-     Elf_Data *data;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagdata (Elf_Data *data, Elf_Cmd cmd, unsigned int flags)
 {
   Elf_Data_Scn *data_scn;
   unsigned int result;
diff --git a/elfutils/libelf/elf_flagehdr.c b/elfutils/libelf/elf_flagehdr.c
index 5a1d37a89..00dea4b47 100644
--- a/elfutils/libelf/elf_flagehdr.c
+++ b/elfutils/libelf/elf_flagehdr.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagehdr (elf, cmd, flags)
-     Elf *elf;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagehdr (Elf *elf, Elf_Cmd cmd, unsigned int flags)
 {
   unsigned int result;
 
diff --git a/elfutils/libelf/elf_flagelf.c b/elfutils/libelf/elf_flagelf.c
index 6eb780d26..153df67e6 100644
--- a/elfutils/libelf/elf_flagelf.c
+++ b/elfutils/libelf/elf_flagelf.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagelf (elf, cmd, flags)
-     Elf *elf;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagelf (Elf *elf, Elf_Cmd cmd, unsigned int flags)
 {
   unsigned int result;
 
diff --git a/elfutils/libelf/elf_flagphdr.c b/elfutils/libelf/elf_flagphdr.c
index f5753919b..f9a9258f9 100644
--- a/elfutils/libelf/elf_flagphdr.c
+++ b/elfutils/libelf/elf_flagphdr.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagphdr (elf, cmd, flags)
-     Elf *elf;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagphdr (Elf *elf, Elf_Cmd cmd, unsigned int flags)
 {
   unsigned int result;
 
diff --git a/elfutils/libelf/elf_flagscn.c b/elfutils/libelf/elf_flagscn.c
index 74adfb5b2..269525902 100644
--- a/elfutils/libelf/elf_flagscn.c
+++ b/elfutils/libelf/elf_flagscn.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagscn (scn, cmd, flags)
-     Elf_Scn *scn;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagscn (Elf_Scn *scn, Elf_Cmd cmd, unsigned int flags)
 {
   unsigned int result;
 
diff --git a/elfutils/libelf/elf_flagshdr.c b/elfutils/libelf/elf_flagshdr.c
index e32724a82..047d84ee1 100644
--- a/elfutils/libelf/elf_flagshdr.c
+++ b/elfutils/libelf/elf_flagshdr.c
@@ -26,10 +26,7 @@
 
 
 unsigned int
-elf_flagshdr (scn, cmd, flags)
-     Elf_Scn *scn;
-     Elf_Cmd cmd;
-     unsigned int flags;
+elf_flagshdr (Elf_Scn *scn, Elf_Cmd cmd, unsigned int flags)
 {
   unsigned int result;
 
diff --git a/elfutils/libelf/elf_getarhdr.c b/elfutils/libelf/elf_getarhdr.c
index b301676b9..4a725fe35 100644
--- a/elfutils/libelf/elf_getarhdr.c
+++ b/elfutils/libelf/elf_getarhdr.c
@@ -27,8 +27,7 @@
 
 
 Elf_Arhdr *
-elf_getarhdr (elf)
-     Elf *elf;
+elf_getarhdr (Elf *elf)
 {
   Elf *parent = elf->parent;
 
diff --git a/elfutils/libelf/elf_getarsym.c b/elfutils/libelf/elf_getarsym.c
index 45cddff74..f02efbb78 100644
--- a/elfutils/libelf/elf_getarsym.c
+++ b/elfutils/libelf/elf_getarsym.c
@@ -32,9 +32,7 @@
 
 
 Elf_Arsym *
-elf_getarsym (elf, ptr)
-     Elf *elf;
-     size_t *ptr;
+elf_getarsym (Elf *elf, size_t *ptr)
 {
   Elf_Arsym *result;
 
diff --git a/elfutils/libelf/elf_getbase.c b/elfutils/libelf/elf_getbase.c
index 27f122240..9e4b394aa 100644
--- a/elfutils/libelf/elf_getbase.c
+++ b/elfutils/libelf/elf_getbase.c
@@ -26,8 +26,7 @@
 
 
 off_t
-elf_getbase (elf)
-     Elf *elf;
+elf_getbase (Elf *elf)
 {
   return elf == NULL ? (off_t) -1 : elf->start_offset;
 }
diff --git a/elfutils/libelf/elf_getdata.c b/elfutils/libelf/elf_getdata.c
index f2720d716..938025eaa 100644
--- a/elfutils/libelf/elf_getdata.c
+++ b/elfutils/libelf/elf_getdata.c
@@ -39,6 +39,7 @@
       ? SHT_NUM + Sh_Type - SHT_LOSUNW					      \
       : 0))
 
+/*@unchecked@*/
 static const struct
 {
   Elf_Type type;
@@ -106,6 +107,7 @@ static const struct
 static void
 convert_data (Elf_Scn *scn, int version, int eclass, int data,
 	      size_t size, size_t type)
+	/*@modifies scn @*/
 {
 #if ALLOW_ALIGNED
   /* No need to compute the alignment requirement of the host.  */
@@ -182,7 +184,7 @@ __libelf_set_rawdata (Elf_Scn *scn)
 
   if (elf->class == ELFCLASS32)
     {
-      Elf32_Shdr *shdr = scn->shdr.e32 ?: INTUSE(elf32_getshdr) (scn);
+      Elf32_Shdr *shdr = scn->shdr.e32 ? scn->shdr.e32 : INTUSE(elf32_getshdr) (scn);
 
       if (shdr == NULL)
 	/* Something went terribly wrong.  */
@@ -195,7 +197,7 @@ __libelf_set_rawdata (Elf_Scn *scn)
     }
   else
     {
-      Elf64_Shdr *shdr = scn->shdr.e64 ?: INTUSE(elf64_getshdr) (scn);
+      Elf64_Shdr *shdr = scn->shdr.e64 ? scn->shdr.e64 : INTUSE(elf64_getshdr) (scn);
 
       if (shdr == NULL)
 	/* Something went terribly wrong.  */
@@ -305,9 +307,7 @@ __libelf_set_rawdata (Elf_Scn *scn)
 
 
 Elf_Data *
-elf_getdata (scn, data)
-     Elf_Scn *scn;
-     Elf_Data *data;
+elf_getdata (Elf_Scn *scn, Elf_Data *data)
 {
   Elf_Data *result = NULL;
   Elf *elf;
diff --git a/elfutils/libelf/elf_getident.c b/elfutils/libelf/elf_getident.c
index f2b6b4468..a8d291217 100644
--- a/elfutils/libelf/elf_getident.c
+++ b/elfutils/libelf/elf_getident.c
@@ -25,9 +25,7 @@
 
 
 char *
-elf_getident (elf, ptr)
-     Elf *elf;
-     size_t *ptr;
+elf_getident (Elf *elf, size_t *ptr)
 {
   /* In case this is no ELF file, the handle is invalid and we return
      NULL.  */
diff --git a/elfutils/libelf/elf_getscn.c b/elfutils/libelf/elf_getscn.c
index d52b7a8e2..d8359dd8e 100644
--- a/elfutils/libelf/elf_getscn.c
+++ b/elfutils/libelf/elf_getscn.c
@@ -27,9 +27,7 @@
 
 
 Elf_Scn *
-elf_getscn (elf, index)
-     Elf *elf;
-     size_t index;
+elf_getscn (Elf *elf, size_t index)
 {
   Elf_Scn *result = NULL;
   Elf_ScnList *runp;
diff --git a/elfutils/libelf/elf_getshnum.c b/elfutils/libelf/elf_getshnum.c
index a540ce392..63d3ba3c9 100644
--- a/elfutils/libelf/elf_getshnum.c
+++ b/elfutils/libelf/elf_getshnum.c
@@ -27,9 +27,7 @@
 
 
 int
-elf_getshnum (elf, dst)
-     Elf *elf;
-     size_t *dst;
+elf_getshnum (Elf *elf, size_t *dst)
 {
   int result = 0;
   int idx;
diff --git a/elfutils/libelf/elf_getshstrndx.c b/elfutils/libelf/elf_getshstrndx.c
index dac89e942..f340832d1 100644
--- a/elfutils/libelf/elf_getshstrndx.c
+++ b/elfutils/libelf/elf_getshstrndx.c
@@ -32,9 +32,7 @@
 #endif
 
 int
-elf_getshstrndx (elf, dst)
-     Elf *elf;
-     size_t *dst;
+elf_getshstrndx (Elf *elf, size_t *dst)
 {
   int result = 0;
 
diff --git a/elfutils/libelf/elf_hash.c b/elfutils/libelf/elf_hash.c
index fb0abc834..8437ffd27 100644
--- a/elfutils/libelf/elf_hash.c
+++ b/elfutils/libelf/elf_hash.c
@@ -25,8 +25,7 @@
 #include <dl-hash.h>
 
 unsigned long int
-elf_hash (string)
-     const char *string;
+elf_hash (const char *string)
 {
   return _dl_elf_hash (string);
 }
diff --git a/elfutils/libelf/elf_kind.c b/elfutils/libelf/elf_kind.c
index f3f0d58c7..9c1fef7ec 100644
--- a/elfutils/libelf/elf_kind.c
+++ b/elfutils/libelf/elf_kind.c
@@ -26,8 +26,7 @@
 
 
 Elf_Kind
-elf_kind (elf)
-     Elf *elf;
+elf_kind (Elf *elf)
 {
   return elf == NULL ? ELF_K_NONE : elf->kind;
 }
diff --git a/elfutils/libelf/elf_memory.c b/elfutils/libelf/elf_memory.c
index 2ab9b1b2a..a5a32aef0 100644
--- a/elfutils/libelf/elf_memory.c
+++ b/elfutils/libelf/elf_memory.c
@@ -26,9 +26,7 @@
 
 
 Elf *
-elf_memory (image, size)
-     char *image;
-     size_t size;
+elf_memory (char *image, size_t size)
 {
   if (image == NULL)
     {
diff --git a/elfutils/libelf/elf_ndxscn.c b/elfutils/libelf/elf_ndxscn.c
index 52cc92962..f527a3a4e 100644
--- a/elfutils/libelf/elf_ndxscn.c
+++ b/elfutils/libelf/elf_ndxscn.c
@@ -26,8 +26,7 @@
 
 
 size_t
-elf_ndxscn (scn)
-     Elf_Scn *scn;
+elf_ndxscn (Elf_Scn *scn)
 {
   if (scn == NULL)
     return SHN_UNDEF;
diff --git a/elfutils/libelf/elf_newscn.c b/elfutils/libelf/elf_newscn.c
index 5968d02dc..8f84988c3 100644
--- a/elfutils/libelf/elf_newscn.c
+++ b/elfutils/libelf/elf_newscn.c
@@ -29,8 +29,7 @@
 
 
 Elf_Scn *
-elf_newscn (elf)
-     Elf *elf;
+elf_newscn (Elf *elf)
 {
   Elf_Scn *result = NULL;
   bool first = false;
diff --git a/elfutils/libelf/elf_next.c b/elfutils/libelf/elf_next.c
index 126130c2d..113498c14 100644
--- a/elfutils/libelf/elf_next.c
+++ b/elfutils/libelf/elf_next.c
@@ -27,8 +27,7 @@
 
 
 Elf_Cmd
-elf_next (elf)
-     Elf *elf;
+elf_next (Elf *elf)
 {
   Elf *parent;
 
diff --git a/elfutils/libelf/elf_nextscn.c b/elfutils/libelf/elf_nextscn.c
index f8d6e5eac..4bf1a5a03 100644
--- a/elfutils/libelf/elf_nextscn.c
+++ b/elfutils/libelf/elf_nextscn.c
@@ -27,9 +27,7 @@
 
 
 Elf_Scn *
-elf_nextscn (elf, scn)
-     Elf *elf;
-     Elf_Scn *scn;
+elf_nextscn (Elf *elf, Elf_Scn *scn)
 {
   Elf_Scn *result = NULL;
 
@@ -46,12 +44,12 @@ elf_nextscn (elf, scn)
 	       == offsetof (Elf, state.elf64.scns)))
 	{
 	  if (elf->state.elf32.scns.cnt > 1)
-	    result = &elf->state.elf32.scns.data[0];
+	    result = &elf->state.elf32.scns.data[1];
 	}
       else
 	{
 	  if (elf->state.elf64.scns.cnt > 1)
-	    result = &elf->state.elf64.scns.data[0];
+	    result = &elf->state.elf64.scns.data[1];
 	}
     }
   else
diff --git a/elfutils/libelf/elf_rand.c b/elfutils/libelf/elf_rand.c
index b18f80227..b6a560e4e 100644
--- a/elfutils/libelf/elf_rand.c
+++ b/elfutils/libelf/elf_rand.c
@@ -26,9 +26,7 @@
 
 
 size_t
-elf_rand (elf, offset)
-     Elf *elf;
-     size_t offset;
+elf_rand (Elf *elf, size_t offset)
 {
   /* Be gratious, the specs demand it.  */
   if (elf == NULL || elf->kind != ELF_K_AR)
diff --git a/elfutils/libelf/elf_rawdata.c b/elfutils/libelf/elf_rawdata.c
index 7ac2e25a7..c795e0f9d 100644
--- a/elfutils/libelf/elf_rawdata.c
+++ b/elfutils/libelf/elf_rawdata.c
@@ -25,9 +25,7 @@
 
 
 Elf_Data *
-elf_rawdata (scn, data)
-     Elf_Scn *scn;
-     Elf_Data *data;
+elf_rawdata (Elf_Scn *scn, Elf_Data *data)
 {
   if (scn == NULL || scn->elf->kind != ELF_K_ELF)
     {
diff --git a/elfutils/libelf/elf_rawfile.c b/elfutils/libelf/elf_rawfile.c
index 10f29a044..c99c745a0 100644
--- a/elfutils/libelf/elf_rawfile.c
+++ b/elfutils/libelf/elf_rawfile.c
@@ -26,9 +26,7 @@
 
 
 char *
-elf_rawfile (elf, ptr)
-     Elf *elf;
-     size_t *ptr;
+elf_rawfile (Elf *elf, size_t *ptr)
 {
   if (elf == NULL)
     {
diff --git a/elfutils/libelf/elf_readall.c b/elfutils/libelf/elf_readall.c
index 3d54355be..da87f9ca6 100644
--- a/elfutils/libelf/elf_readall.c
+++ b/elfutils/libelf/elf_readall.c
@@ -27,6 +27,7 @@
 
 static void
 set_address (Elf *elf, size_t offset)
+	/*@modifies elf @*/
 {
   if (elf->kind == ELF_K_AR)
     {
@@ -51,8 +52,8 @@ set_address (Elf *elf, size_t offset)
 
 
 char *
-__libelf_readall (elf)
-     Elf *elf;
+internal_function
+__libelf_readall (Elf *elf)
 {
   /* Get the file.  */
   rwlock_wrlock (elf->lock);
diff --git a/elfutils/libelf/elf_strptr.c b/elfutils/libelf/elf_strptr.c
index 2ed81c9ec..d19165f45 100644
--- a/elfutils/libelf/elf_strptr.c
+++ b/elfutils/libelf/elf_strptr.c
@@ -26,10 +26,7 @@
 
 
 char *
-elf_strptr (elf, index, offset)
-     Elf *elf;
-     size_t index;
-     size_t offset;
+elf_strptr (Elf *elf, size_t index, size_t offset)
 {
   char *result = NULL;
   Elf_ScnList *runp;
diff --git a/elfutils/libelf/elf_update.c b/elfutils/libelf/elf_update.c
index bcf285c94..1cb6602a3 100644
--- a/elfutils/libelf/elf_update.c
+++ b/elfutils/libelf/elf_update.c
@@ -28,6 +28,7 @@
 
 static off_t
 write_file (Elf *elf, off_t size, int change_bo, size_t shnum)
+	/*@modifies elf @*/
 {
   int class = elf->class;
 
@@ -90,9 +91,7 @@ write_file (Elf *elf, off_t size, int change_bo, size_t shnum)
 
 
 off_t
-elf_update (elf, cmd)
-     Elf *elf;
-     Elf_Cmd cmd;
+elf_update (Elf *elf, Elf_Cmd cmd)
 {
   size_t shnum;
   off_t size;
diff --git a/elfutils/libelf/elf_version.c b/elfutils/libelf/elf_version.c
index 388d71c6e..0a0451fe0 100644
--- a/elfutils/libelf/elf_version.c
+++ b/elfutils/libelf/elf_version.c
@@ -29,9 +29,9 @@ int __libelf_version_initialized;
 unsigned int __libelf_version = EV_CURRENT;
 
 
+/*@-mods@*/
 unsigned int
-elf_version (version)
-     unsigned int version;
+elf_version (unsigned int version)
 {
   if (version == EV_NONE)
     return __libelf_version;
@@ -55,4 +55,5 @@ elf_version (version)
   __libelf_seterrno (ELF_E_UNKNOWN_VERSION);
   return EV_NONE;
 }
+/*@=mods@*/
 INTDEF(elf_version)
diff --git a/elfutils/libelf/gelf.h b/elfutils/libelf/gelf.h
index a563acb11..cc838fae9 100644
--- a/elfutils/libelf/gelf.h
+++ b/elfutils/libelf/gelf.h
@@ -131,151 +131,218 @@ typedef Elf64_Move GElf_Move;
 
 
 /* Get class of the file associated with ELF.  */
-extern int gelf_getclass (Elf *__elf);
+extern int gelf_getclass (Elf *__elf)
+	/*@*/;
 
 
 /* Return size of array of COUNT elemeents of the type denoted by TYPE
    in the external representation.  The binary class is taken from ELF.
    The result is based on version VERSION of the ELF standard.  */
 extern size_t gelf_fsize (Elf *__elf, Elf_Type __type, size_t __count,
-			  unsigned int __version);
+			  unsigned int __version)
+	/*@*/;
 
 /* Retrieve object file header.  */
-extern GElf_Ehdr *gelf_getehdr (Elf *__elf, GElf_Ehdr *__dest);
+/*@null@*/
+extern GElf_Ehdr *gelf_getehdr (Elf *elf, /*@returned@*/ /*@out@*/ GElf_Ehdr *dest)
+	/*@modifies elf, dest @*/;
 
 /* Update the ELF header.  */
-extern int gelf_update_ehdr (Elf *__elf, GElf_Ehdr *__src);
+extern int gelf_update_ehdr (Elf *elf, GElf_Ehdr *__src)
+	/*@modifies elf @*/;
 
 /* Create new ELF header if none exists.  */
-extern unsigned long int gelf_newehdr (Elf *__elf, int __class);
+extern unsigned long int gelf_newehdr (Elf *elf, int __class)
+	/*@modifies elf @*/;
 
 /* Retrieve section header.  */
-extern GElf_Shdr *gelf_getshdr (Elf_Scn *__scn, GElf_Shdr *__dst);
+/*@null@*/
+extern GElf_Shdr *gelf_getshdr (Elf_Scn *scn,
+				/*@returned@*/ /*@out@*/ GElf_Shdr *dst)
+	/*@modifies scn, dst @*/;
 
 /* Update section header.  */
-extern int gelf_update_shdr (Elf_Scn *__scn, GElf_Shdr *__src);
+extern int gelf_update_shdr (Elf_Scn *scn, GElf_Shdr *__src)
+	/*@modifies scn @*/;
 
 /* Retrieve program header table entry.  */
-extern GElf_Phdr *gelf_getphdr (Elf *__elf, int __ndx, GElf_Phdr *__dst);
+extern GElf_Phdr *gelf_getphdr (Elf *elf, int __ndx,
+				/*@returned@*/ /*@out@*/ GElf_Phdr *dst)
+	/*@modifies elf, dst @*/;
 
 /* Update the program header.  */
-extern int gelf_update_phdr (Elf *__elf, int __ndx, GElf_Phdr *__src);
+extern int gelf_update_phdr (Elf *elf, int __ndx, GElf_Phdr *__src)
+	/*@modifies elf @*/;
 
 /* Create new program header with PHNUM entries.  */
-extern unsigned long int gelf_newphdr (Elf *__elf, size_t __phnum);
+extern unsigned long int gelf_newphdr (Elf *elf, size_t __phnum)
+	/*@modifies elf @*/;
 
 
 /* Convert data structure from the representation in the file represented
    by ELF to their memory representation.  */
-extern Elf_Data *gelf_xlatetom (Elf *__elf, Elf_Data *__dest,
-				const Elf_Data *__src, unsigned int __encode);
+extern Elf_Data *gelf_xlatetom (Elf *__elf, Elf_Data *dest,
+				const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 
 /* Convert data structure from to the representation in memory
    represented by ELF file representation.  */
-extern Elf_Data *gelf_xlatetof (Elf *__elf, Elf_Data *__dest,
-				const Elf_Data *__src, unsigned int __encode);
+extern Elf_Data *gelf_xlatetof (Elf *__elf, Elf_Data *dest,
+				const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 
 
 /* Retrieve REL relocation info at the given index.  */
-extern GElf_Rel *gelf_getrel (Elf_Data *__data, int __ndx, GElf_Rel *__dst);
+/*@null@*/
+extern GElf_Rel *gelf_getrel (Elf_Data *__data, int __ndx,
+			      /*@returned@*/ /*@out@*/ GElf_Rel *dst)
+	/*@modifies dst @*/;
 
 /* Retrieve RELA relocation info at the given index.  */
-extern GElf_Rela *gelf_getrela (Elf_Data *__data, int __ndx, GElf_Rela *__dst);
+/*@null@*/
+extern GElf_Rela *gelf_getrela (Elf_Data *__data, int __ndx,
+				/*@returned@*/ /*@out@*/ GElf_Rela *dst)
+	/*@modifies dst @*/;
 
 /* Update REL relocation information at given index.  */
-extern int gelf_update_rel (Elf_Data *__dst, int __ndx, GElf_Rel *__src);
+extern int gelf_update_rel (Elf_Data *__dst, int __ndx, GElf_Rel *__src)
+	/*@*/;
 
 /* Update RELA relocation information at given index.  */
-extern int gelf_update_rela (Elf_Data *__dst, int __ndx, GElf_Rela *__src);
+extern int gelf_update_rela (Elf_Data *__dst, int __ndx, GElf_Rela *__src)
+	/*@*/;
 
 
 /* Retrieve symbol information from the symbol table at the given index.  */
-extern GElf_Sym *gelf_getsym (Elf_Data *__data, int __ndx, GElf_Sym *__dst);
+/*@null@*/
+extern GElf_Sym *gelf_getsym (Elf_Data *__data, int __ndx,
+			      /*@returned@*/ /*@out@*/ GElf_Sym *dst)
+	/*@modifies dst @*/;
 
 /* Update symbol information in the symbol table at the given index.  */
-extern int gelf_update_sym (Elf_Data *__data, int __ndx, GElf_Sym *__src);
+extern int gelf_update_sym (Elf_Data *__data, int __ndx, GElf_Sym *__src)
+	/*@*/;
 
 
 /* Retrieve symbol information and separate section index from the
    symbol table at the given index.  */
+/*@null@*/
 extern GElf_Sym *gelf_getsymshndx (Elf_Data *__symdata, Elf_Data *__shndxdata,
-				   int __ndx, GElf_Sym *__sym,
-				   Elf32_Word *__xshndx);
+				   int __ndx, GElf_Sym *dst,
+				   Elf32_Word *dstshndx)
+	/*@modifies dst, dstshndx @*/;
 
 /* Update symbol information and separate section index in the symbol
    table at the given index.  */
 extern int gelf_update_symshndx (Elf_Data *__symdata, Elf_Data *__shndxdata,
 				 int __ndx, GElf_Sym *__sym,
-				 Elf32_Word __xshndx);
+				 Elf32_Word __xshndx)
+	/*@*/;
 
 
 /* Retrieve additional symbol information from the symbol table at the
    given index.  */
+/*@null@*/
 extern GElf_Syminfo *gelf_getsyminfo (Elf_Data *__data, int __ndx,
-				      GElf_Syminfo *__dst);
+				      /*@returned@*/ /*@out@*/ GElf_Syminfo *dst)
+	/*@modifies dst @*/;
 
 /* Update additional symbol information in the symbol table at the
    given index.  */
 extern int gelf_update_syminfo (Elf_Data *__data, int __ndx,
-				GElf_Syminfo *__src);
+				GElf_Syminfo *__src)
+	/*@*/;
 
 
 /* Get information from dynamic table at the given index.  */
-extern GElf_Dyn *gelf_getdyn (Elf_Data *__data, int __ndx, GElf_Dyn *__dst);
+/*@null@*/
+extern GElf_Dyn *gelf_getdyn (Elf_Data *__data, int __ndx,
+			      /*@returned@*/ /*@out@*/ GElf_Dyn *dst)
+	/*@modifies dst @*/;
 
 /* Update information in dynamic table at the given index.  */
-extern int gelf_update_dyn (Elf_Data *__dst, int __ndx, GElf_Dyn *__src);
+extern int gelf_update_dyn (Elf_Data *__dst, int __ndx, GElf_Dyn *__src)
+	/*@*/;
 
 
 /* Get move structure at the given index.  */
-extern GElf_Move *gelf_getmove (Elf_Data *__data, int __ndx, GElf_Move *__dst);
+/*@null@*/
+extern GElf_Move *gelf_getmove (Elf_Data *__data, int __ndx,
+				/*@returned@*/ /*@out@*/ GElf_Move *dst)
+	/*@modifies dst @*/;
 
 /* Update move structure at the given index.  */
 extern int gelf_update_move (Elf_Data *__data, int __ndx,
-			     GElf_Move *__src);
+			     GElf_Move *__src)
+	/*@*/;
 
 
 /* Retrieve symbol version information at given index.  */
+/*@null@*/
 extern GElf_Versym *gelf_getversym (Elf_Data *__data, int __ndx,
-				    GElf_Versym *__dst);
+				    /*@returned@*/ /*@out@*/ GElf_Versym *dst)
+	/*@modifies dst @*/;
 
 /* Update symbol version information.  */
-extern int gelf_update_versym (Elf_Data *__data, int __ndx, GElf_Versym __src);
+extern int gelf_update_versym (Elf_Data *__data, int __ndx, GElf_Versym __src)
+	/*@*/;
 
 
 /* Retrieve required symbol version information at given offset.  */
+/*@null@*/
 extern GElf_Verneed *gelf_getverneed (Elf_Data *__data, int __offset,
-				      GElf_Verneed *__dst);
+				      /*@returned@*/ /*@out@*/ GElf_Verneed *dst)
+	/*@modifies dst @*/;
 
 /* Update required symbol version information.  */
 extern int gelf_update_verneed (Elf_Data *__data, int __offset,
-				GElf_Verneed *__src);
+				GElf_Verneed *__src)
+	/*@*/;
 
 /* Retrieve additional required symbol version information at given offset.  */
+/*@null@*/
 extern GElf_Vernaux *gelf_getvernaux (Elf_Data *__data, int __offset,
-				      GElf_Vernaux *__dst);
+				      /*@returned@*/ /*@out@*/ GElf_Vernaux *dst)
+	/*@modifies dst @*/;
 
 /* Update additional required symbol version information.  */
 extern int gelf_update_vernaux (Elf_Data *__data, int __offset,
-				GElf_Vernaux *__src);
+				GElf_Vernaux *__src)
+	/*@*/;
 
 
 /* Retrieve symbol version definition information at given offset.  */
+/*@null@*/
 extern GElf_Verdef *gelf_getverdef (Elf_Data *__data, int __offset,
-				    GElf_Verdef *__dst);
+				    /*@returned@*/ /*@out@*/ GElf_Verdef *dst)
+	/*@modifies dst @*/;
 
 /* Update symbol version definition information.  */
 extern int gelf_update_verdef (Elf_Data *__data, int __offset,
-			       GElf_Verdef *__src);
+			       GElf_Verdef *__src)
+	/*@*/;
 
 /* Retrieve additional symbol version definition information at given
    offset.  */
+/*@null@*/
 extern GElf_Verdaux *gelf_getverdaux (Elf_Data *__data, int __offset,
-				      GElf_Verdaux *__dst);
+				      /*@returned@*/ /*@out@*/ GElf_Verdaux *dst)
+	/*@modifies dst @*/;
 
 /* Update additional symbol version definition information.  */
 extern int gelf_update_verdaux (Elf_Data *__data, int __offset,
-				GElf_Verdaux *__src);
+				GElf_Verdaux *__src)
+	/*@*/;
+
+
+/* Retrieve uninterpreted chunk of the file contents.  */
+/*@null@*/
+extern char *gelf_rawchunk (Elf *__elf, GElf_Off __offset, GElf_Word __size)
+	/*@*/;
+
+/* Release uninterpreted chunk of the file contents.  */
+extern void gelf_freechunk (Elf *__elf, /*@only@*/ char *ptr)
+	/*@modifies ptr @*/;
 
 #ifdef __cplusplus
 }
diff --git a/elfutils/libelf/gelf_checksum.c b/elfutils/libelf/gelf_checksum.c
index 558619358..c77fdf9ac 100644
--- a/elfutils/libelf/gelf_checksum.c
+++ b/elfutils/libelf/gelf_checksum.c
@@ -26,8 +26,8 @@
 
 
 long int
-gelf_checksum (elf)
-     Elf *elf;
+gelf_checksum (Elf *elf)
+	/*@modifies elf @*/
 {
   if (elf == NULL)
     return -1l;
diff --git a/elfutils/libelf/gelf_freechunk.c b/elfutils/libelf/gelf_freechunk.c
index 5b35eff51..1408f4425 100644
--- a/elfutils/libelf/gelf_freechunk.c
+++ b/elfutils/libelf/gelf_freechunk.c
@@ -27,9 +27,7 @@
 
 
 void
-gelf_freechunk (elf, ptr)
-     Elf *elf;
-     char *ptr;
+gelf_freechunk (Elf *elf, char *ptr)
 {
   if (elf == NULL)
     /* No valid descriptor.  */
diff --git a/elfutils/libelf/gelf_fsize.c b/elfutils/libelf/gelf_fsize.c
index eed078ac2..fc6faa0bc 100644
--- a/elfutils/libelf/gelf_fsize.c
+++ b/elfutils/libelf/gelf_fsize.c
@@ -64,11 +64,7 @@ const size_t __libelf_type_sizes[EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM] =
 
 
 size_t
-gelf_fsize (elf, type, count, version)
-     Elf *elf;
-     Elf_Type type;
-     size_t count;
-     unsigned int version;
+gelf_fsize (Elf *elf, Elf_Type type, size_t count, unsigned int version)
 {
   /* We do not have differences between file and memory sizes.  Better
      not since otherwise `mmap' would not work.  */
diff --git a/elfutils/libelf/gelf_getclass.c b/elfutils/libelf/gelf_getclass.c
index 02ba48075..af5008824 100644
--- a/elfutils/libelf/gelf_getclass.c
+++ b/elfutils/libelf/gelf_getclass.c
@@ -26,8 +26,7 @@
 
 
 int
-gelf_getclass (elf)
-     Elf *elf;
+gelf_getclass (Elf *elf)
 {
   return elf == NULL || elf->kind != ELF_K_ELF ? ELFCLASSNONE : elf->class;
 }
diff --git a/elfutils/libelf/gelf_getdyn.c b/elfutils/libelf/gelf_getdyn.c
index 8c6e3f680..20905fbaa 100644
--- a/elfutils/libelf/gelf_getdyn.c
+++ b/elfutils/libelf/gelf_getdyn.c
@@ -27,10 +27,7 @@
 
 
 GElf_Dyn *
-gelf_getdyn (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Dyn *dst;
+gelf_getdyn (Elf_Data *data, int ndx, GElf_Dyn *dst)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   GElf_Dyn *result = NULL;
diff --git a/elfutils/libelf/gelf_getehdr.c b/elfutils/libelf/gelf_getehdr.c
index 964ae2140..08ddea715 100644
--- a/elfutils/libelf/gelf_getehdr.c
+++ b/elfutils/libelf/gelf_getehdr.c
@@ -26,9 +26,7 @@
 
 
 GElf_Ehdr *
-gelf_getehdr (elf, dest)
-     Elf *elf;
-     GElf_Ehdr *dest;
+gelf_getehdr (Elf *elf, GElf_Ehdr *dest)
 {
   GElf_Ehdr *result = NULL;
 
diff --git a/elfutils/libelf/gelf_getmove.c b/elfutils/libelf/gelf_getmove.c
index e5f1d19a8..79e50a530 100644
--- a/elfutils/libelf/gelf_getmove.c
+++ b/elfutils/libelf/gelf_getmove.c
@@ -27,10 +27,7 @@
 
 
 GElf_Move *
-gelf_getmove (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Move *dst;
+gelf_getmove (Elf_Data *data, int ndx, GElf_Move *dst)
 {
   GElf_Move *result = NULL;
   Elf *elf;
diff --git a/elfutils/libelf/gelf_getphdr.c b/elfutils/libelf/gelf_getphdr.c
index 8c7474e05..a2081df67 100644
--- a/elfutils/libelf/gelf_getphdr.c
+++ b/elfutils/libelf/gelf_getphdr.c
@@ -26,10 +26,7 @@
 
 
 GElf_Phdr *
-gelf_getphdr (elf, ndx, dst)
-     Elf *elf;
-     int ndx;
-     GElf_Phdr *dst;
+gelf_getphdr (Elf *elf, int ndx, GElf_Phdr *dst)
 {
   GElf_Phdr *result = NULL;
 
diff --git a/elfutils/libelf/gelf_getrel.c b/elfutils/libelf/gelf_getrel.c
index bbb2635f1..f8269b21d 100644
--- a/elfutils/libelf/gelf_getrel.c
+++ b/elfutils/libelf/gelf_getrel.c
@@ -26,10 +26,7 @@
 
 
 GElf_Rel *
-gelf_getrel (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Rel *dst;
+gelf_getrel (Elf_Data *data, int ndx, GElf_Rel *dst)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_getrela.c b/elfutils/libelf/gelf_getrela.c
index 94dfcdf61..83a1e90a5 100644
--- a/elfutils/libelf/gelf_getrela.c
+++ b/elfutils/libelf/gelf_getrela.c
@@ -26,10 +26,7 @@
 
 
 GElf_Rela *
-gelf_getrela (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Rela *dst;
+gelf_getrela (Elf_Data *data, int ndx, GElf_Rela *dst)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_getshdr.c b/elfutils/libelf/gelf_getshdr.c
index 18183e1dc..e7b28fdf0 100644
--- a/elfutils/libelf/gelf_getshdr.c
+++ b/elfutils/libelf/gelf_getshdr.c
@@ -26,9 +26,7 @@
 
 
 GElf_Shdr *
-gelf_getshdr (scn, dst)
-     Elf_Scn *scn;
-     GElf_Shdr *dst;
+gelf_getshdr (Elf_Scn *scn, GElf_Shdr *dst)
 {
   GElf_Shdr *result = NULL;
 
@@ -46,7 +44,7 @@ gelf_getshdr (scn, dst)
   if (scn->elf->class == ELFCLASS32)
     {
       /* Copy the elements one-by-one.  */
-      Elf32_Shdr *shdr = scn->shdr.e32 ?: INTUSE(elf32_getshdr) (scn);
+      Elf32_Shdr *shdr = scn->shdr.e32 ? scn->shdr.e32 : INTUSE(elf32_getshdr) (scn);
 
       if (shdr == NULL)
 	{
@@ -71,7 +69,7 @@ gelf_getshdr (scn, dst)
     }
   else
     {
-      Elf64_Shdr *shdr = scn->shdr.e64 ?: INTUSE(elf64_getshdr) (scn);
+      Elf64_Shdr *shdr = scn->shdr.e64 ? scn->shdr.e64 : INTUSE(elf64_getshdr) (scn);
 
       if (shdr == NULL)
 	{
diff --git a/elfutils/libelf/gelf_getsym.c b/elfutils/libelf/gelf_getsym.c
index c99ad820f..a90e7a3aa 100644
--- a/elfutils/libelf/gelf_getsym.c
+++ b/elfutils/libelf/gelf_getsym.c
@@ -27,10 +27,7 @@
 
 
 GElf_Sym *
-gelf_getsym (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Sym *dst;
+gelf_getsym (Elf_Data *data, int ndx, GElf_Sym *dst)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   GElf_Sym *result = NULL;
diff --git a/elfutils/libelf/gelf_getsyminfo.c b/elfutils/libelf/gelf_getsyminfo.c
index 3020f679d..e3f2250c4 100644
--- a/elfutils/libelf/gelf_getsyminfo.c
+++ b/elfutils/libelf/gelf_getsyminfo.c
@@ -27,10 +27,7 @@
 
 
 GElf_Syminfo *
-gelf_getsyminfo (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Syminfo *dst;
+gelf_getsyminfo (Elf_Data *data, int ndx, GElf_Syminfo *dst)
 {
   GElf_Syminfo *result = NULL;
 
diff --git a/elfutils/libelf/gelf_getsymshndx.c b/elfutils/libelf/gelf_getsymshndx.c
index d8180cfd6..88b4cab57 100644
--- a/elfutils/libelf/gelf_getsymshndx.c
+++ b/elfutils/libelf/gelf_getsymshndx.c
@@ -28,12 +28,8 @@
 
 
 GElf_Sym *
-gelf_getsymshndx (symdata, shndxdata, ndx, dst, dstshndx)
-     Elf_Data *symdata;
-     Elf_Data *shndxdata;
-     int ndx;
-     GElf_Sym *dst;
-     Elf32_Word *dstshndx;
+gelf_getsymshndx (Elf_Data *symdata, Elf_Data *shndxdata, int ndx,
+		  GElf_Sym *dst, Elf32_Word *dstshndx)
 {
   Elf_Data_Scn *symdata_scn = (Elf_Data_Scn *) symdata;
   Elf_Data_Scn *shndxdata_scn = (Elf_Data_Scn *) shndxdata;
diff --git a/elfutils/libelf/gelf_getverdaux.c b/elfutils/libelf/gelf_getverdaux.c
index 2fd4ea796..b4b431b04 100644
--- a/elfutils/libelf/gelf_getverdaux.c
+++ b/elfutils/libelf/gelf_getverdaux.c
@@ -27,10 +27,7 @@
 
 
 GElf_Verdaux *
-gelf_getverdaux (data, offset, dst)
-     Elf_Data *data;
-     int offset;
-     GElf_Verdaux *dst;
+gelf_getverdaux (Elf_Data *data, int offset, GElf_Verdaux *dst)
 {
   GElf_Verdaux *result;
 
diff --git a/elfutils/libelf/gelf_getverdef.c b/elfutils/libelf/gelf_getverdef.c
index 866592a68..36340c5cf 100644
--- a/elfutils/libelf/gelf_getverdef.c
+++ b/elfutils/libelf/gelf_getverdef.c
@@ -27,10 +27,7 @@
 
 
 GElf_Verdef *
-gelf_getverdef (data, offset, dst)
-     Elf_Data *data;
-     int offset;
-     GElf_Verdef *dst;
+gelf_getverdef (Elf_Data *data, int offset, GElf_Verdef *dst)
 {
   GElf_Verdef *result;
 
diff --git a/elfutils/libelf/gelf_getvernaux.c b/elfutils/libelf/gelf_getvernaux.c
index 142c36a62..7e4ffcef2 100644
--- a/elfutils/libelf/gelf_getvernaux.c
+++ b/elfutils/libelf/gelf_getvernaux.c
@@ -27,10 +27,7 @@
 
 
 GElf_Vernaux *
-gelf_getvernaux (data, offset, dst)
-     Elf_Data *data;
-     int offset;
-     GElf_Vernaux *dst;
+gelf_getvernaux (Elf_Data *data, int offset, GElf_Vernaux *dst)
 {
   GElf_Vernaux *result;
 
diff --git a/elfutils/libelf/gelf_getverneed.c b/elfutils/libelf/gelf_getverneed.c
index d02e509ae..a3b0613a2 100644
--- a/elfutils/libelf/gelf_getverneed.c
+++ b/elfutils/libelf/gelf_getverneed.c
@@ -27,10 +27,7 @@
 
 
 GElf_Verneed *
-gelf_getverneed (data, offset, dst)
-     Elf_Data *data;
-     int offset;
-     GElf_Verneed *dst;
+gelf_getverneed (Elf_Data *data, int offset, GElf_Verneed *dst)
 {
   GElf_Verneed *result;
 
diff --git a/elfutils/libelf/gelf_getversym.c b/elfutils/libelf/gelf_getversym.c
index ddc807e8a..460d01118 100644
--- a/elfutils/libelf/gelf_getversym.c
+++ b/elfutils/libelf/gelf_getversym.c
@@ -27,10 +27,7 @@
 
 
 GElf_Versym *
-gelf_getversym (data, ndx, dst)
-     Elf_Data *data;
-     int ndx;
-     GElf_Versym *dst;
+gelf_getversym (Elf_Data *data, int ndx, GElf_Versym *dst)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_newehdr.c b/elfutils/libelf/gelf_newehdr.c
index 0233bb8e5..23ab57862 100644
--- a/elfutils/libelf/gelf_newehdr.c
+++ b/elfutils/libelf/gelf_newehdr.c
@@ -26,9 +26,7 @@
 
 
 unsigned long int
-gelf_newehdr (elf, class)
-     Elf *elf;
-     int class;
+gelf_newehdr (Elf *elf, int class)
 {
   return (class == ELFCLASS32
 	  ? (unsigned long int) INTUSE(elf32_newehdr) (elf)
diff --git a/elfutils/libelf/gelf_newphdr.c b/elfutils/libelf/gelf_newphdr.c
index 090f34391..3e4def117 100644
--- a/elfutils/libelf/gelf_newphdr.c
+++ b/elfutils/libelf/gelf_newphdr.c
@@ -26,9 +26,7 @@
 
 
 unsigned long int
-gelf_newphdr (elf, phnum)
-     Elf *elf;
-     size_t phnum;
+gelf_newphdr (Elf *elf, size_t phnum)
 {
   return (elf->class == ELFCLASS32
 	  ? (unsigned long int) INTUSE(elf32_newphdr) (elf, phnum)
diff --git a/elfutils/libelf/gelf_rawchunk.c b/elfutils/libelf/gelf_rawchunk.c
index 056552d96..e64b0e8a6 100644
--- a/elfutils/libelf/gelf_rawchunk.c
+++ b/elfutils/libelf/gelf_rawchunk.c
@@ -28,11 +28,9 @@
 
 
 char *
-gelf_rawchunk (elf, offset, size)
-     Elf *elf;
-     GElf_Off offset;
-     GElf_Word size;
+gelf_rawchunk (Elf *elf, GElf_Off offset, GElf_Word size)
 {
+  char * result;
   if (elf == NULL)
     {
       /* No valid descriptor.  */
@@ -54,7 +52,7 @@ gelf_rawchunk (elf, offset, size)
     return (char *) elf->map_address + elf->start_offset + offset;
 
   /* We allocate the memory and read the data from the file.  */
-  char *result = (char *) malloc (size);
+  result = (char *) malloc (size);
   if (result == NULL)
     __libelf_seterrno (ELF_E_NOMEM);
   else
diff --git a/elfutils/libelf/gelf_update_dyn.c b/elfutils/libelf/gelf_update_dyn.c
index 76773cada..6d51c0b46 100644
--- a/elfutils/libelf/gelf_update_dyn.c
+++ b/elfutils/libelf/gelf_update_dyn.c
@@ -26,10 +26,7 @@
 
 
 int
-gelf_update_dyn (data, ndx, src)
-     Elf_Data *data;
-     int ndx;
-     GElf_Dyn *src;
+gelf_update_dyn (Elf_Data *data, int ndx, GElf_Dyn *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_update_move.c b/elfutils/libelf/gelf_update_move.c
index cb9dd2073..a3103e621 100644
--- a/elfutils/libelf/gelf_update_move.c
+++ b/elfutils/libelf/gelf_update_move.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_move (data, ndx, src)
-     Elf_Data *data;
-     int ndx;
-     GElf_Move *src;
+gelf_update_move (Elf_Data *data, int ndx, GElf_Move *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_update_shdr.c b/elfutils/libelf/gelf_update_shdr.c
index 9471d5372..34397e6b7 100644
--- a/elfutils/libelf/gelf_update_shdr.c
+++ b/elfutils/libelf/gelf_update_shdr.c
@@ -39,7 +39,7 @@ gelf_update_shdr (Elf_Scn *scn, GElf_Shdr *src)
 
   if (elf->class == ELFCLASS32)
     {
-      Elf32_Shdr *shdr = scn->shdr.e32 ?: INTUSE(elf32_getshdr) (scn);
+      Elf32_Shdr *shdr = scn->shdr.e32 ? scn->shdr.e32 : INTUSE(elf32_getshdr) (scn);
 
       if (shdr == NULL)
 	{
@@ -73,7 +73,7 @@ gelf_update_shdr (Elf_Scn *scn, GElf_Shdr *src)
     }
   else
     {
-      Elf64_Shdr *shdr = scn->shdr.e64 ?: INTUSE(elf64_getshdr) (scn);
+      Elf64_Shdr *shdr = scn->shdr.e64 ? scn->shdr.e64 : INTUSE(elf64_getshdr) (scn);
 
       if (shdr == NULL)
 	{
diff --git a/elfutils/libelf/gelf_update_sym.c b/elfutils/libelf/gelf_update_sym.c
index d8a862b6e..44b099de0 100644
--- a/elfutils/libelf/gelf_update_sym.c
+++ b/elfutils/libelf/gelf_update_sym.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_sym (data, ndx, src)
-     Elf_Data *data;
-     int ndx;
-     GElf_Sym *src;
+gelf_update_sym (Elf_Data *data, int ndx, GElf_Sym *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_update_syminfo.c b/elfutils/libelf/gelf_update_syminfo.c
index a6e330b0b..30deca746 100644
--- a/elfutils/libelf/gelf_update_syminfo.c
+++ b/elfutils/libelf/gelf_update_syminfo.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_syminfo (data, ndx, src)
-     Elf_Data *data;
-     int ndx;
-     GElf_Syminfo *src;
+gelf_update_syminfo (Elf_Data *data, int ndx, GElf_Syminfo *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
   Elf_Scn *scn;
diff --git a/elfutils/libelf/gelf_update_symshndx.c b/elfutils/libelf/gelf_update_symshndx.c
index b47d1a79c..9b0510292 100644
--- a/elfutils/libelf/gelf_update_symshndx.c
+++ b/elfutils/libelf/gelf_update_symshndx.c
@@ -28,12 +28,8 @@
 
 
 int
-gelf_update_symshndx (symdata, shndxdata, ndx, src, srcshndx)
-     Elf_Data *symdata;
-     Elf_Data *shndxdata;
-     int ndx;
-     GElf_Sym *src;
-     Elf32_Word srcshndx;
+gelf_update_symshndx (Elf_Data *symdata, Elf_Data *shndxdata, int ndx,
+		      GElf_Sym *src, Elf32_Word srcshndx)
 {
   Elf_Data_Scn *symdata_scn = (Elf_Data_Scn *) symdata;
   Elf_Data_Scn *shndxdata_scn = (Elf_Data_Scn *) shndxdata;
diff --git a/elfutils/libelf/gelf_update_verdaux.c b/elfutils/libelf/gelf_update_verdaux.c
index 967621da6..1993a283e 100644
--- a/elfutils/libelf/gelf_update_verdaux.c
+++ b/elfutils/libelf/gelf_update_verdaux.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_verdaux (data, offset, src)
-     Elf_Data *data;
-     int offset;
-     GElf_Verdaux *src;
+gelf_update_verdaux (Elf_Data *data, int offset, GElf_Verdaux *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_update_verdef.c b/elfutils/libelf/gelf_update_verdef.c
index 11d28a206..fc5c6e89d 100644
--- a/elfutils/libelf/gelf_update_verdef.c
+++ b/elfutils/libelf/gelf_update_verdef.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_verdef (data, offset, src)
-     Elf_Data *data;
-     int offset;
-     GElf_Verdef *src;
+gelf_update_verdef (Elf_Data *data, int offset, GElf_Verdef *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_update_vernaux.c b/elfutils/libelf/gelf_update_vernaux.c
index 180186305..23dd23bd4 100644
--- a/elfutils/libelf/gelf_update_vernaux.c
+++ b/elfutils/libelf/gelf_update_vernaux.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_vernaux (data, offset, src)
-     Elf_Data *data;
-     int offset;
-     GElf_Vernaux *src;
+gelf_update_vernaux (Elf_Data *data, int offset, GElf_Vernaux *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_update_verneed.c b/elfutils/libelf/gelf_update_verneed.c
index 26c87f7bf..22bca6722 100644
--- a/elfutils/libelf/gelf_update_verneed.c
+++ b/elfutils/libelf/gelf_update_verneed.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_verneed (data, offset, src)
-     Elf_Data *data;
-     int offset;
-     GElf_Verneed *src;
+gelf_update_verneed (Elf_Data *data, int offset, GElf_Verneed *src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_update_versym.c b/elfutils/libelf/gelf_update_versym.c
index e8a6eac4c..3c15188fe 100644
--- a/elfutils/libelf/gelf_update_versym.c
+++ b/elfutils/libelf/gelf_update_versym.c
@@ -27,10 +27,7 @@
 
 
 int
-gelf_update_versym (data, ndx, src)
-     Elf_Data *data;
-     int ndx;
-     GElf_Versym src;
+gelf_update_versym (Elf_Data *data, int ndx, GElf_Versym src)
 {
   Elf_Data_Scn *data_scn = (Elf_Data_Scn *) data;
 
diff --git a/elfutils/libelf/gelf_xlate.c b/elfutils/libelf/gelf_xlate.c
index 460a789ac..3ab625889 100644
--- a/elfutils/libelf/gelf_xlate.c
+++ b/elfutils/libelf/gelf_xlate.c
@@ -37,6 +37,7 @@
    : Elf32_cvt_Byte (dest, src, n))
 static void
 (elf_cvt_Byte) (void *dest, const void *src, size_t n, int encode)
+	/*@modifies dest @*/
 {
   memmove (dest, src, n);
 }
@@ -170,7 +171,10 @@ const xfct_t __elf_xfctstom[EV_NUM - 1][EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM]
     }
   }
 };
+
+#if !defined(__LCLINT__)
 /* For now we only handle the case where the memory representation is the
    same as the file representation.  Should this change we have to define
    separate functions.  For now reuse them.  */
 strong_alias (__elf_xfctstom, __elf_xfctstof)
+#endif
diff --git a/elfutils/libelf/gelf_xlate.h b/elfutils/libelf/gelf_xlate.h
index 14a55ec2c..7624d5721 100644
--- a/elfutils/libelf/gelf_xlate.h
+++ b/elfutils/libelf/gelf_xlate.h
@@ -17,6 +17,7 @@
 
 
 /* Simple types.  */
+/*@-mods@*/
 FUNDAMENTAL (ADDR, Addr, LIBELFBITS);
 FUNDAMENTAL (OFF, Off, LIBELFBITS);
 FUNDAMENTAL (HALF, Half, LIBELFBITS);
@@ -24,8 +25,10 @@ FUNDAMENTAL (WORD, Word, LIBELFBITS);
 FUNDAMENTAL (SWORD, Sword, LIBELFBITS);
 FUNDAMENTAL (XWORD, Xword, LIBELFBITS);
 FUNDAMENTAL (SXWORD, Sxword, LIBELFBITS);
+/*@=mods@*/
 
 /* The strctured types.  */
+/*@-modunconnomods -noeffectuncon@*/
 TYPE (Ehdr, LIBELFBITS)
 TYPE (Phdr, LIBELFBITS)
 TYPE (Shdr, LIBELFBITS)
@@ -36,6 +39,7 @@ TYPE (Note, LIBELFBITS)
 TYPE (Dyn, LIBELFBITS)
 TYPE (Syminfo, LIBELFBITS)
 TYPE (Move, LIBELFBITS)
+/*@=modunconnomods =noeffectuncon@*/
 
 
 /* Prepare for the next round.  */
diff --git a/elfutils/libelf/gelf_xlatetof.c b/elfutils/libelf/gelf_xlatetof.c
index afc944ad2..28768c4cc 100644
--- a/elfutils/libelf/gelf_xlatetof.c
+++ b/elfutils/libelf/gelf_xlatetof.c
@@ -26,11 +26,8 @@
 
 
 Elf_Data *
-gelf_xlatetof (elf, dest, src, encode)
-     Elf *elf;
-     Elf_Data *dest;
-     const Elf_Data * src;
-     unsigned int encode;
+gelf_xlatetof (Elf *elf, Elf_Data *dest, const Elf_Data * src,
+	       unsigned int encode)
 {
   if (elf == NULL)
     return NULL;
diff --git a/elfutils/libelf/gelf_xlatetom.c b/elfutils/libelf/gelf_xlatetom.c
index ecd088ff4..9d60dd52c 100644
--- a/elfutils/libelf/gelf_xlatetom.c
+++ b/elfutils/libelf/gelf_xlatetom.c
@@ -26,11 +26,8 @@
 
 
 Elf_Data *
-gelf_xlatetom (elf, dest, src, encode)
-     Elf *elf;
-     Elf_Data *dest;
-     const Elf_Data * src;
-     unsigned int encode;
+gelf_xlatetom (Elf *elf, Elf_Data *dest, const Elf_Data * src,
+	       unsigned int encode)
 {
   if (elf == NULL)
     return NULL;
diff --git a/elfutils/libelf/libelf.h b/elfutils/libelf/libelf.h
index 7a4b61d37..d933d5602 100644
--- a/elfutils/libelf/libelf.h
+++ b/elfutils/libelf/libelf.h
@@ -144,133 +144,180 @@ extern "C" {
 #endif
 
 /* Return descriptor for ELF file to work according to CMD.  */
-extern Elf *elf_begin (int __fildes, Elf_Cmd __cmd, Elf *__ref);
+/*@only@*/ /*@null@*/
+extern Elf *elf_begin (int __fildes, Elf_Cmd __cmd,
+		       /*@returned@*/ /*@null@*/ Elf *ref)
+	/*@modifies ref @*/;
 
 /* Create descriptor for memory region.  */
-extern Elf *elf_memory (char *__image, size_t __size);
+/*@null@*/
+extern Elf *elf_memory (char *__image, size_t __size)
+	/*@*/;
 
 /* Advance archive descriptor to next element.  */
-extern Elf_Cmd elf_next (Elf *__elf);
+extern Elf_Cmd elf_next (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Free resources allocated for ELF.  */
-extern int elf_end (Elf *__elf);
+extern int elf_end (/*@only@*/ /*@null@*/ Elf *elf)
+	/*@modifies elf @*/;
 
 /* Update ELF descriptor and write file to disk.  */
-extern off_t elf_update (Elf *__elf, Elf_Cmd __cmd);
+extern off_t elf_update (Elf *elf, Elf_Cmd __cmd)
+	/*@modifies elf @*/;
 
 /* Determine what kind of file is associated with ELF.  */
-extern Elf_Kind elf_kind (Elf *__elf) __attribute__ ((__pure__));
+extern Elf_Kind elf_kind (Elf *__elf) __attribute__ ((__pure__))
+	/*@*/;
 
 /* Get the base offset for an object file.  */
-extern off_t elf_getbase (Elf *__elf);
+extern off_t elf_getbase (Elf *__elf)
+	/*@*/;
 
 
 /* Retrieve file identification data.  */
-extern char *elf_getident (Elf *__elf, size_t *__ptr);
+extern char *elf_getident (Elf *__elf, size_t *ptr)
+	/*@modifies *ptr @*/;
 
 /* Retrieve class-dependent object file header.  */
-extern Elf32_Ehdr *elf32_getehdr (Elf *__elf);
+extern Elf32_Ehdr *elf32_getehdr (Elf *elf)
+	/*@modifies elf @*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
-extern Elf64_Ehdr *elf64_getehdr (Elf *__elf);
+extern Elf64_Ehdr *elf64_getehdr (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Create ELF header if none exists.  */
-extern Elf32_Ehdr *elf32_newehdr (Elf *__elf);
+extern Elf32_Ehdr *elf32_newehdr (Elf *elf)
+	/*@modifies elf @*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
-extern Elf64_Ehdr *elf64_newehdr (Elf *__elf);
+extern Elf64_Ehdr *elf64_newehdr (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Retrieve class-dependent program header table.  */
-extern Elf32_Phdr *elf32_getphdr (Elf *__elf);
+extern Elf32_Phdr *elf32_getphdr (Elf *elf)
+	/*@modifies elf @*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
-extern Elf64_Phdr *elf64_getphdr (Elf *__elf);
+extern Elf64_Phdr *elf64_getphdr (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Create ELF program header.  */
-extern Elf32_Phdr *elf32_newphdr (Elf *__elf, size_t __cnt);
+/*@null@*/
+extern Elf32_Phdr *elf32_newphdr (Elf *elf, size_t __cnt)
+	/*@modifies elf @*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
-extern Elf64_Phdr *elf64_newphdr (Elf *__elf, size_t __cnt);
+/*@null@*/
+extern Elf64_Phdr *elf64_newphdr (Elf *elf, size_t __cnt)
+	/*@modifies elf @*/;
 
 
 /* Get section at INDEX.  */
-extern Elf_Scn *elf_getscn (Elf *__elf, size_t __index);
+extern Elf_Scn *elf_getscn (Elf *__elf, size_t __index)
+	/*@*/;
 
 /* Get index of section.  */
-extern size_t elf_ndxscn (Elf_Scn *__scn);
+extern size_t elf_ndxscn (Elf_Scn *__scn)
+	/*@*/;
 
 /* Get section with next section index.  */
-extern Elf_Scn *elf_nextscn (Elf *__elf, Elf_Scn *__scn);
+extern Elf_Scn *elf_nextscn (Elf *__elf, Elf_Scn *__scn)
+	/*@*/;
 
 /* Create a new section and append it at the end of the table.  */
-extern Elf_Scn *elf_newscn (Elf *__elf);
+extern Elf_Scn *elf_newscn (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Get the number of sections in the ELF file.  If the file uses more
    sections than can be represented in the e_shnum field of the ELF
    header the information from the sh_size field in the zeroth section
    header is used.  */
-extern int elf_getshnum (Elf *__elf, size_t *__dst);
+extern int elf_getshnum (Elf *__elf, /*@out@*/ size_t *dst)
+	/*@modifies *dst @*/;
 
 
 /* Get the section index of the section header string table in the ELF
    file.  If the index cannot be represented in the e_shnum field of
    the ELF header the information from the sh_link field in the zeroth
    section header is used.  */
-extern int elf_getshstrndx (Elf *__elf, size_t *__dst);
+extern int elf_getshstrndx (Elf *__elf, /*@out@*/ size_t *dst)
+	/*@modifies *dst @*/;
 
 
 /* Retrieve section header of ELFCLASS32 binary.  */
-extern Elf32_Shdr *elf32_getshdr (Elf_Scn *__scn);
+extern Elf32_Shdr *elf32_getshdr (Elf_Scn *scn)
+	/*@modifies scn @*/;
 /* Similar for ELFCLASS64.  */
-extern Elf64_Shdr *elf64_getshdr (Elf_Scn *__scn);
+extern Elf64_Shdr *elf64_getshdr (Elf_Scn *scn)
+	/*@modifies scn @*/;
 
 
 /* Set or clear flags for ELF file.  */
-extern unsigned int elf_flagelf (Elf *__elf, Elf_Cmd __cmd,
-				 unsigned int __flags);
+extern unsigned int elf_flagelf (Elf *elf, Elf_Cmd __cmd,
+				 unsigned int __flags)
+	/*@modifies elf @*/;
 /* Similarly for the ELF header.  */
-extern unsigned int elf_flagehdr (Elf *__elf, Elf_Cmd __cmd,
-				  unsigned int __flags);
+extern unsigned int elf_flagehdr (Elf *elf, Elf_Cmd __cmd,
+				  unsigned int __flags)
+	/*@modifies elf @*/;
 /* Similarly for the ELF program header.  */
-extern unsigned int elf_flagphdr (Elf *__elf, Elf_Cmd __cmd,
-				  unsigned int __flags);
+extern unsigned int elf_flagphdr (Elf *elf, Elf_Cmd __cmd,
+				  unsigned int __flags)
+	/*@modifies elf @*/;
 /* Similarly for the given ELF section.  */
-extern unsigned int elf_flagscn (Elf_Scn *__scn, Elf_Cmd __cmd,
-				 unsigned int __flags);
+extern unsigned int elf_flagscn (Elf_Scn *scn, Elf_Cmd __cmd,
+				 unsigned int __flags)
+	/*@modifies scn @*/;
 /* Similarly for the given ELF data.  */
 extern unsigned int elf_flagdata (Elf_Data *__data, Elf_Cmd __cmd,
-				  unsigned int __flags);
+				  unsigned int __flags)
+	/*@*/;
 /* Similarly for the given ELF section header.  */
-extern unsigned int elf_flagshdr (Elf_Scn *__scn, Elf_Cmd __cmd,
-				  unsigned int __flags);
+extern unsigned int elf_flagshdr (Elf_Scn *scn, Elf_Cmd __cmd,
+				  unsigned int __flags)
+	/*@modifies scn @*/;
 
 
 /* Get data from section while translating from file representation
    to memory representation.  */
-extern Elf_Data *elf_getdata (Elf_Scn *__scn, Elf_Data *__data);
+/*@null@*/
+extern Elf_Data *elf_getdata (Elf_Scn *scn, /*@null@*/ Elf_Data *__data)
+	/*@modifies scn @*/;
 
 /* Get uninterpreted section content.  */
-extern Elf_Data *elf_rawdata (Elf_Scn *__scn, Elf_Data *__data);
+extern Elf_Data *elf_rawdata (Elf_Scn *scn, Elf_Data *__data)
+	/*@modifies scn @*/;
 
 /* Create new data descriptor for section SCN.  */
-extern Elf_Data *elf_newdata (Elf_Scn *__scn);
+extern Elf_Data *elf_newdata (Elf_Scn *scn)
+	/*@modifies scn @*/;
 
 
 /* Return pointer to string at OFFSET in section INDEX.  */
-extern char *elf_strptr (Elf *__elf, size_t __index, size_t __offset);
+/*@dependent@*/ /*@null@*/
+extern char *elf_strptr (Elf *elf, size_t __index, size_t __offset)
+	/*@modifies elf @*/;
 
 
 /* Return header of archive.  */
-extern Elf_Arhdr *elf_getarhdr (Elf *__elf);
+extern Elf_Arhdr *elf_getarhdr (Elf *elf)
+	/*@modifies elf @*/;
 
 /* Select archive element at OFFSET.  */
-extern size_t elf_rand (Elf *__elf, size_t __offset);
+extern size_t elf_rand (Elf *elf, size_t __offset)
+	/*@modifies elf @*/;
 
 /* Get symbol table of archhive.  */
-extern Elf_Arsym *elf_getarsym (Elf *__elf, size_t *__ptr);
+/*@null@*/
+extern Elf_Arsym *elf_getarsym (Elf *elf, /*@out@*/ size_t *ptr)
+	/*@modifies elf, ptr @*/;
 
 
 /* Control ELF descriptor.  */
-extern int elf_cntl (Elf *__elf, Elf_Cmd __cmd);
+extern int elf_cntl (Elf *elf, Elf_Cmd __cmd)
+	/*@modifies elf @*/;
 
 /* Retrieve uninterpreted file contents.  */
-extern char *elf_rawfile (Elf *__elf, size_t *__ptr);
+extern char *elf_rawfile (Elf *elf, size_t *ptr)
+	/*@modifies elf, *ptr @*/;
 
 
 /* Return size of array of COUNT elements of the type denoted by TYPE
@@ -278,56 +325,70 @@ extern char *elf_rawfile (Elf *__elf, size_t *__ptr);
    The result is based on version VERSION of the ELF standard.  */
 extern size_t elf32_fsize (Elf_Type __type, size_t __count,
 			   unsigned int __version)
-       __attribute__ ((__const__));
+       __attribute__ ((__const__))
+	/*@*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
 extern size_t elf64_fsize (Elf_Type __type, size_t __count,
 			   unsigned int __version)
-       __attribute__ ((__const__));
+       __attribute__ ((__const__))
+	/*@*/;
 
 
 /* Convert data structure from the representation in the file represented
    by ELF to their memory representation.  */
-extern Elf_Data *elf32_xlatetom (Elf_Data *__dest, const Elf_Data *__src,
-				 unsigned int __encode);
+extern Elf_Data *elf32_xlatetom (/*@returned@*/ Elf_Data *dest,
+				 const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 /* Same for 64 bit class.  */
-extern Elf_Data *elf64_xlatetom (Elf_Data *__dest, const Elf_Data *__src,
-				 unsigned int __encode);
+extern Elf_Data *elf64_xlatetom (/*@returned@*/ Elf_Data *dest,
+				 const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 
 /* Convert data structure from to the representation in memory
    represented by ELF file representation.  */
-extern Elf_Data *elf32_xlatetof (Elf_Data *__dest, const Elf_Data *__src,
-				 unsigned int __encode);
+extern Elf_Data *elf32_xlatetof (/*@returned@*/ Elf_Data *dest,
+				 const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 /* Same for 64 bit class.  */
-extern Elf_Data *elf64_xlatetof (Elf_Data *__dest, const Elf_Data *__src,
-				 unsigned int __encode);
+extern Elf_Data *elf64_xlatetof (/*@returned@*/ Elf_Data *dest,
+				 const Elf_Data *__src, unsigned int __encode)
+	/*@modifies dest @*/;
 
 
 /* Return error code of last failing function call.  This value is kept
    separately for each thread.  */
-extern int elf_errno (void);
+extern int elf_errno (void)
+	/*@*/;
 
 /* Return error string for ERROR.  If ERROR is zero, return error string
    for most recent error or NULL is none occurred.  If ERROR is -1 the
    behaviour is similar to the last case except that not NULL but a legal
    string is returned.  */
-extern const char *elf_errmsg (int __error);
+extern const char *elf_errmsg (int __error)
+	/*@*/;
 
 
 /* Coordinate ELF library and application versions.  */
-extern unsigned int elf_version (unsigned int __version);
+extern unsigned int elf_version (unsigned int __version)
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
 
 /* Set fill bytes used to fill holes in data structures.  */
-extern void elf_fill (int __fill);
+extern void elf_fill (int __fill)
+	/*@*/;
 
 /* Compute hash value.  */
 extern unsigned long int elf_hash (const char *__string)
-       __attribute__ ((__pure__));
+       __attribute__ ((__pure__))
+	/*@*/;
 
 
 /* Compute simple checksum from permanent parts of the ELF file.  */
-extern long int elf32_checksum (Elf *__elf);
+extern long int elf32_checksum (Elf *elf)
+	/*@modifies elf @*/;
 /* Similar but this time the binary calls is ELFCLASS64.  */
-extern long int elf64_checksum (Elf *__elf);
+extern long int elf64_checksum (Elf *elf)
+	/*@modifies elf @*/;
 
 #ifdef __cplusplus
 }
diff --git a/elfutils/libelf/libelfP.h b/elfutils/libelf/libelfP.h
index 8a1c76355..48032b409 100644
--- a/elfutils/libelf/libelfP.h
+++ b/elfutils/libelf/libelfP.h
@@ -22,6 +22,10 @@
 #include <gelf.h>
 #include <stdint.h>
 
+#if defined(__LCLINT__)
+typedef int bool;
+#endif
+
 /* gettext helper macros.  */
 #define _(Str) dgettext ("libelf", Str)
 
@@ -242,6 +246,7 @@ struct Elf
   size_t maximum_size;
 
   /* Address to which the file was mapped.  NULL if not mapped.  */
+/*@null@*/
   void *map_address;
 
   /* Describes the way the memory was allocated and if the dirty bit is
@@ -251,6 +256,7 @@ struct Elf
 
   /* When created for an archive member this points to the descriptor
      for the archive. */
+/*@null@*/
   Elf *parent;
 
   /* Lock to handle multithreaded programs.  */
@@ -353,15 +359,19 @@ struct Elf
 
 /* Type of the conversion functions.  These functions will convert the
    byte order.  */
-typedef void (*xfct_t) (void *, const void *, size_t, int);
+typedef void (*xfct_t) (void *, const void *, size_t, int)
+	/*@*/;
 
 /* The table with the function pointers.  */
+/*@unchecked@*/
 extern const xfct_t __elf_xfctstom[EV_NUM - 1][EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM] attribute_hidden;
+/*@unchecked@*/
 extern const xfct_t __elf_xfctstof[EV_NUM - 1][EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM] attribute_hidden;
 
 
 /* Array with sizes of the external types indexed by ELF version, binary
    class, and type. */
+/*@unchecked@*/
 extern const size_t __libelf_type_sizes[EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM] attribute_hidden;
 /* We often have to access the size for a type in the current version.  */
 #if EV_NUM != 2
@@ -373,12 +383,15 @@ extern const size_t __libelf_type_sizes[EV_NUM - 1][ELFCLASSNUM - 1][ELF_T_NUM]
 #endif
 
 /* Currently selected version of the ELF specification.  */
+/*@unchecked@*/
 extern unsigned int __libelf_version attribute_hidden;
 
 /* The byte value used for filling gaps.  */
+/*@unchecked@*/
 extern int __libelf_fill_byte attribute_hidden;
 
 /* Nonzero if the version was set.  */
+/*@unchecked@*/
 extern int __libelf_version_initialized attribute_hidden;
 
 
@@ -388,109 +401,155 @@ extern int __libelf_version_initialized attribute_hidden;
    These functions cannot be marked internal since they are aliases
    of the export elfXX_fsize functions.*/
 extern size_t __elf32_msize (Elf_Type __type, size_t __count,
-			     unsigned int __version);
+			     unsigned int __version)
+	/*@*/;
 extern size_t __elf64_msize (Elf_Type __type, size_t __count,
-			     unsigned int __version);
+			     unsigned int __version)
+	/*@*/;
 
 
 /* Create Elf descriptor from memory image.  */
+/*@null@*/
 extern Elf *__libelf_read_mmaped_file (int fildes, void *map_address,
 				       off_t offset, size_t maxsize,
-				       Elf_Cmd cmd, Elf *parent)
-     internal_function;
+				       Elf_Cmd cmd, /*@null@*/ Elf *parent)
+     internal_function
+	/*@*/;
 
 /* Set error value.  */
-extern void __libelf_seterrno (int value) internal_function;
+extern void __libelf_seterrno (int value) internal_function
+	/*@globals internalState @*/
+	/*@modifies internalState @*/;
 
 /* Get the next archive header.  */
-extern int __libelf_next_arhdr (Elf *elf) internal_function;
+extern int __libelf_next_arhdr (Elf *elf) internal_function
+	/*@modifies elf @*/;
 
 /* Read all of the file associated with the descriptor.  */
-extern char *__libelf_readall (Elf *elf) internal_function;
+/*@null@*/
+extern char *__libelf_readall (Elf *elf) internal_function
+	/*@modifies elf @*/;
 
 /* Read the complete section table and convert the byte order if necessary.  */
-extern int __libelf_readsections (Elf *elf) internal_function;
+extern int __libelf_readsections (Elf *elf) internal_function
+	/*@*/;
 
 /* Store the information for the raw data in the `rawdata_list' element.  */
-extern int __libelf_set_rawdata (Elf_Scn *scn) internal_function;
+extern int __libelf_set_rawdata (Elf_Scn *scn) internal_function
+	/*@modifies scn @*/;
 
 
 /* Helper functions for elf_update.  */
 extern off_t __elf32_updatenull (Elf *elf, int *change_bop, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf, *change_bop @*/;
 extern off_t __elf64_updatenull (Elf *elf, int *change_bop, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf, *change_bop @*/;
 
 extern int __elf32_updatemmap (Elf *elf, int change_bo, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf @*/;
 extern int __elf64_updatemmap (Elf *elf, int change_bo, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf @*/;
 extern int __elf32_updatefile (Elf *elf, int change_bo, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf @*/;
 extern int __elf64_updatefile (Elf *elf, int change_bo, size_t shnum)
-     internal_function;
+     internal_function
+	/*@modifies elf @*/;
 
 
 /* Alias for exported functions to avoid PLT entries.  */
 extern Elf *__elf_begin_internal (int __fildes, Elf_Cmd __cmd, Elf *__ref)
-     attribute_hidden;
-extern Elf32_Ehdr *__elf32_getehdr_internal (Elf *__elf) attribute_hidden;
-extern Elf64_Ehdr *__elf64_getehdr_internal (Elf *__elf) attribute_hidden;
-extern Elf32_Ehdr *__elf32_newehdr_internal (Elf *__elf) attribute_hidden;
-extern Elf64_Ehdr *__elf64_newehdr_internal (Elf *__elf) attribute_hidden;
-extern Elf32_Phdr *__elf32_getphdr_internal (Elf *__elf) attribute_hidden;
-extern Elf64_Phdr *__elf64_getphdr_internal (Elf *__elf) attribute_hidden;
+     attribute_hidden
+	/*@*/;
+extern Elf32_Ehdr *__elf32_getehdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern Elf64_Ehdr *__elf64_getehdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern Elf32_Ehdr *__elf32_newehdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern Elf64_Ehdr *__elf64_newehdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern Elf32_Phdr *__elf32_getphdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern Elf64_Phdr *__elf64_getphdr_internal (Elf *__elf) attribute_hidden
+	/*@*/;
 extern Elf32_Phdr *__elf32_newphdr_internal (Elf *__elf, size_t __cnt)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf64_Phdr *__elf64_newphdr_internal (Elf *__elf, size_t __cnt)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern int __elf_getshnum_internal (Elf *__elf, size_t *__dst)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern int __elf_getshstrndx_internal (Elf *__elf, size_t *__dst)
-     attribute_hidden;
-extern Elf32_Shdr *__elf32_getshdr_internal (Elf_Scn *__scn) attribute_hidden;
-extern Elf64_Shdr *__elf64_getshdr_internal (Elf_Scn *__scn) attribute_hidden;
+     attribute_hidden
+	/*@*/;
+extern Elf32_Shdr *__elf32_getshdr_internal (Elf_Scn *__scn) attribute_hidden
+	/*@*/;
+extern Elf64_Shdr *__elf64_getshdr_internal (Elf_Scn *__scn) attribute_hidden
+	/*@*/;
 extern Elf_Scn *__elf_getscn_internal (Elf *__elf, size_t __index)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Scn *__elf_nextscn_internal (Elf *__elf, Elf_Scn *__scn)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf_getdata_internal (Elf_Scn *__scn, Elf_Data *__data)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf_rawdata_internal (Elf_Scn *__scn, Elf_Data *__data)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern char *__elf_strptr_internal (Elf *__elf, size_t __index,
-				    size_t __offset) attribute_hidden;
+				    size_t __offset) attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf32_xlatetom_internal (Elf_Data *__dest,
 					    const Elf_Data *__src,
 					    unsigned int __encode)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf64_xlatetom_internal (Elf_Data *__dest,
 					    const Elf_Data *__src,
 					    unsigned int __encode)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf32_xlatetof_internal (Elf_Data *__dest,
 					    const Elf_Data *__src,
 					    unsigned int __encode)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern Elf_Data *__elf64_xlatetof_internal (Elf_Data *__dest,
 					    const Elf_Data *__src,
 					    unsigned int __encode)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern unsigned int __elf_version_internal (unsigned int __version)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern unsigned long int __elf_hash_internal (const char *__string)
-       __attribute__ ((__pure__, visibility ("hidden")));
-extern long int __elf32_checksum_internal (Elf *__elf) attribute_hidden;
-extern long int __elf64_checksum_internal (Elf *__elf) attribute_hidden;
+       __attribute__ ((__pure__, visibility ("hidden")))
+	/*@*/;
+extern long int __elf32_checksum_internal (Elf *__elf) attribute_hidden
+	/*@*/;
+extern long int __elf64_checksum_internal (Elf *__elf) attribute_hidden
+	/*@*/;
 
 
 extern size_t __gelf_fsize_internal (Elf *__elf, Elf_Type __type,
 				     size_t __count, unsigned int __version)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern GElf_Shdr *__gelf_getshdr_internal (Elf_Scn *__scn, GElf_Shdr *__dst)
-     attribute_hidden;
+     attribute_hidden
+	/*@*/;
 extern GElf_Sym *__gelf_getsym_internal (Elf_Data *__data, int __ndx,
-					 GElf_Sym *__dst) attribute_hidden;
+					 GElf_Sym *__dst) attribute_hidden
+	/*@*/;
 
 
 /* We often have to update a flag iff a value changed.  Make this
diff --git a/elfutils/libelf/nlist.h b/elfutils/libelf/nlist.h
index 5c111dd97..0f1c4689d 100644
--- a/elfutils/libelf/nlist.h
+++ b/elfutils/libelf/nlist.h
@@ -35,7 +35,8 @@ extern "C" {
 #endif
 
 /* Get specified entries from file.  */
-extern int nlist (__const char *__filename, struct nlist *__nl);
+extern int nlist (__const char *__filename, struct nlist *nl)
+	/*@modifies *nl @*/;
 
 #ifdef __cplusplus
 }