cgood first taskhelp wanted
Métricas do repositório
- Stars
- (12.410 stars)
- Métricas de merge de PR
- (Mesclagem média 2d 7h) (9 fundiu PRs em 30d)
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.