c - 关闭结构中的文件指针后夹板涉嫌内存泄漏

我正在尝试学习如何使用夹板，同时还尝试重新学习C.安全第一！

我有一个带有文件指针的结构。文件指针在构造函数内打开，在析构函数内关闭。它在结构类型定义中用/@only@/注释，夹板似乎识别出结构内的文件指针是指向该内存的唯一指针（请参见下面的详细信息）。

在析构函数中，只要文件指针不为null，则关闭文件。

但是，夹板似乎在抱怨文件指针未释放，导致内存泄漏，即使只要文件指针!= NULL关闭了文件也是如此。

这是代码：

#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;

}

并导致以下错误：

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)

第二个错误：为什么夹板即使通过filestruct->file也没有在File_close中关闭它？

最佳答案

预防警告

首先，可以通过将file的声明更改为使用/*@dependent@*/而不是/*@only@*/注释来避免这两种警告：

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

为什么这样可以防止错误

关于将dependent存储分配给only存储的第一个错误，之所以引起这个问题，是因为fopen使用的带注释的splint函数在其声明中包括了/*@dependent@*/注释，这与在/*@only@*中定义file的注释。

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

换句话说，夹板抱怨从FileStructure输出的dependent文件指针已分配给fopen变量。

解决此问题还解决了第二个错误，该错误是关于不从内部对象only释放内存的，因为如splint manual中所指定：


程序员应确保从属引用的生存期包含在相应拥有的引用的生存期之内。”（第5.2.3节）


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

至于实际的问题，为什么夹板认为存在未释放的存储，考虑到夹板使用的带注释的file声明，答案就在夹板的输出中：


夹板假定何时有物体
作为外部对象将作为唯一的void指针传递
释放，但内部对象不会。


“仅无效指针”是指夹板使用的带注释的free()函数：

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

这意味着free()在输入filestruct时被视为“仅空指针”，因此假定其内部对象未释放。

我很惊讶，夹板没有弄清楚内部对象在调用free之前已经释放了几行，但这也许仅仅是夹板告诉我们对内部对象使用free()或dependent批注的方式。

参考文献：


有关带注释的owned和fopen here的更多详细信息。
splint manual（位于archive.org，因为splint website在撰写本文时已关闭）尤其请参阅第5.2.3节：拥有和从属引用。