3

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?

4

1 回答 1

1

防止警告

首先，可以通过更改fileto use的声明/*@dependent@*/而不是/*@only@*/注释来避免这两个警告：

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

为什么这可以防止错误

关于将dependentstorage分配给 storage 的第一个错误only，这是因为fopenby 使用的带注释的函数在其声明中包含注释，这与splint定义中的注释相反。/*@dependent@*//*@only@*fileFileStructure

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

换句话说，夹板抱怨dependent文件指针输出fopen被分配给一个only变量。

修复此问题还解决了关于不从内部对象释放内存的第二个错误，file 因为如夹板手册中所述：

程序员有责任确保依赖引用的生命周期包含在相应拥有引用的生命周期内。”（第 5.2.3 节）

为什么夹板认为有未释放的存储

至于实际问题，为什么夹板认为有未释放的存储，答案在考虑夹板使用的注释声明时free()夹板的输出：

Splint 假设当一个对象作为仅输出的 void 指针传递时，外部对象将被释放，但内部对象不会。

“out only void pointer”是指free()夹板使用的带注释的函数：

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

当输入到 时，这意味着filestruct被视为“仅输出 void 指针” free，因此假定其内部对象未释放。

我很惊讶 splint 没有弄清楚内部对象在free()被调用前几行就被释放了，但也许这只是 splint 告诉我们使用dependent或owned注释内部对象的方式。

参考：

  • 关于 annotatedfopen和fclose here的更多细节。

  • 夹板手册（在archive.org，因为夹板网站在撰写本文时已关闭）请参阅第 5.2.3 节：拥有和依赖的参考。

于 2015-08-15T11:51:26.147 回答