facebook/infer

fclose builtin not modeled as file resource

Open

#556 opened on Jan 6, 2017

View on GitHub
 (5 comments) (0 reactions) (0 assignees)HTML (12,410 stars) (1,688 forks)batch import
cgood first taskhelp wanted

Description

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.

Contributor guide