facebook/infer

fclose builtin not modeled as file resource

Open

#556 建立於 2017年1月6日

在 GitHub 查看
 (5 留言) (0 反應) (0 負責人)HTML (12,410 star) (1,688 fork)batch import
cgood first taskhelp wanted

描述

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.

貢獻者指南