diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index d05bfae16..ac34fccad 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -212,7 +212,6 @@ void rewind(FILE *stream); int scanf(const char *format, ...); // builtin: modeled internally void setbuf(FILE * __restrict stream, char * __restrict buf); int setitimer(int which, const struct itimerval *__restrict value, struct itimerval *__restrict ovalue); -int setjmp(jmp_buf env); char *setlocale(int category, const char *locale); int setlogin(const char *name); int setpassent(int stayopen); @@ -781,11 +780,6 @@ void rewind(FILE *stream) { tmp = *stream; } -// modeled as just return a nondeterministic value -int setjmp(jmp_buf env) { - return __infer_nondet_int(); -} - // modeled as exit() void longjmp(jmp_buf env, int val) { exit(0);