facebook/infer

fclose builtin not modeled as file resource

开放

#556 创建于 2017年1月6日

 (5 条评论) (0 个反应) (0 位负责人)HTML (1,688 个派生)batch import
cgood first taskhelp wanted

仓库指标

星标
 (12,410 个星标)
PR 合并指标
 (平均合并 2天 7小时) (30 天内合并 9 个 PR)

描述

I noticed that the resource predicate for fclose matches Rmemory Mnew instead of Rfile as expected (PredSymb.re). fclose is modeled as free, but no file attribute is set (compare https://github.com/facebook/infer/blob/master/infer/models/c/src/libc_basic.c#L485 and fopen https://github.com/facebook/infer/blob/master/infer/models/c/src/libc_basic.c#L445).

Is there a particular reason for this? If I set the file attribute for fclose, the OCaml type matches the Rfile that I expect. I.e.,

int fclose(FILE* stream) {                                                          
  int n;                                                                            
  free(stream);                                                                     
  __set_file_attribute(stream);                                                     
  n = __infer_nondet_int();                                                         
  if (n > 0)                                                                        
    return 0;                                                                       
  else                                                                              
    return EOF;                                                                     
}  

Same question for the close model.

贡献者指南