diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index 1c4cb52e1..d05bfae16 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -1726,8 +1726,11 @@ int fgetpos(FILE *__restrict stream, fpos_t *__restrict pos) { int success; FILE tmp; tmp = *stream; - fpos_t t; - *pos = t; + #ifdef __APPLE__ //fpos_t is a long in MacOS, but a struct in Linux. + *pos = __infer_nondet_long(); + #else + pos->__pos = __infer_nondet_long(); + #endif success = __infer_nondet_int(); if(success) return 0; else return -1;