splint alleged memory leak after closing file pointer within stucture

Question

I'm trying to learn how to use splint for while also trying to relearn C. Safety First!

I have a structure with a file pointer within it. The file pointer is opened within a constructor function, and closed within a destructor function. It is annotated with /@only@/ in the structure type definition, and splint seems to recognize that the file pointer within the structure is the only pointer (see details below) to that memory.

In the destructor function, the file is closed as long as the file pointer is not null.

However, splint seems to be complaining that the file pointer is not released, leading to a memory leak, even though the file is closed as long as the filepointer != NULL.

Here is the code:

#include <stdio.h>

struct FileStructure {
  /*@only@*/ FILE *file;
};

static /*@noreturn@*/ void die(const char *message)
{
  if ((bool) errno) {
    perror(message);
  } else {
    printf("ERROR: %s\n",message);
  }
  exit(EXIT_FAILURE);

}

static struct FileStructure *File_open(const char *filename)
{
  struct FileStructure *filestruct = malloc(sizeof(struct FileStructure));
  if(filestruct == NULL) die("Memory error");
  filestruct->file = fopen(filename,"r+");

  if(!filestruct->file) die("Failed to open the file");
  return filestruct;
}

static void File_close(/*@only@*/ struct FileStructure *filestruct)
{
  if(filestruct) {
    if(filestruct->file != NULL ) (void) fclose(filestruct->file);
    free(filestruct);
  }
}

int main(int argc, char *argv[])
{
  struct FileStructure *filestruct;
  char *filename;

  if(argc < 1) die("USAGE: program <filename>");

  filename=argv[1];
  filestruct=File_open(filename);
  File_close(filestruct);
  return 0;

}

And that causes the following errors:

so-splint-fclose.c: (in function File_open)
so-splint-fclose.c:22:3: Dependent storage assigned to only:
                            filestruct->file = fopen(filename, "r+")
  Dependent storage is transferred to a non-dependent reference. (Use
  -dependenttrans to inhibit warning)
so-splint-fclose.c: (in function File_close)
so-splint-fclose.c:32:10: Only storage filestruct->file (type FILE *) derived
    from released storage is not released (memory leak): filestruct
  A storage leak due to incomplete deallocation of a structure or deep pointer
  is suspected. Unshared storage that is reachable from a reference that is
  being deallocated has not yet been deallocated. Splint assumes when an object
  is passed as an out only void pointer that the outer object will be
  deallocated, but the inner objects will not. (Use -compdestroy to inhibit
  warning)

Second error: Why does splint think that filestruct->file has not been closed in File_close even though it has been via fclose?

Answer 1

Preventing the warnings

Firstly, both warnings can be avoided by changing the declaration of file to use /*@dependent@*/ instead of /*@only@*/ annotation:

struct FileStructure {
  /*@dependent@*/ FILE *file;
};

Why this prevents the errors

Regarding the first error about assigning dependent storage to only storage, this is raised because the annotated fopen function used by splint includes a /*@dependent@*/ annotation in its declaration, which is in contrast to the the /*@only@* annotation defining file within FileStructure.

# From splint's lib/standard.h
/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) 

In other words, splint is complaining that the dependent file pointer output from fopen is assigned to an only variable.

Fixing this issue also solves the second error about not releasing the memory from the inner object file because, as specified in the splint manual:

It is up to the programmer to ensure that the lifetime of a dependent reference is contained within the lifetime of the corresponding owned reference." (Section 5.2.3)

Why splint thinks there is unreleased storage

As for the actual question, why splint thinks there is unreleased storage, the answer is in the output from splint when taken in consideration of the annotated declaration of free() used by splint:

Splint assumes when an object is passed as an out only void pointer that the outer object will be deallocated, but the inner objects will not.

The "out only void pointer" is is referring to the annotated free() function used by splint:

# From splint's lib/standard.h
void free( /*@null@*/ /*@out@*/ /*@only@*/ void *p ) /*@modified p@*/;

That means filestruct is treated as an "out only void pointer" when input to free, and therefore its inner objects are assumed to be left unreleased.

I'm surprised splint doesn't figure out that the inner object was released a few lines before free() was called, but maybe this is all just splint's way of telling us to use dependent or owned annotations for inner objects.

References:

• A few more details about annotated fopen and fclose here.

• splint manual (at archive.org because splint website is down at time of writing) See especially section 5.2.3: Owned and dependent references.