facebook / facebook/infer

Question: Does infer know about setjmp/longjmp ?

Open
#1,881 0 comments 0 reactions 0 assignees View on GitHub
question
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

Question:

Infer seems not to recognize that setjmp longjmp can lead to drastic changes in control flow. Is it possible to annotate or add rules in some way for things that I feel should be OK but infer thinks is problematic?

I often end up with code that leads to the following warning from infer:
```
src/eval_cps.c:5245: error: Null Dereference
pointer `reserved` last assigned on line 5244 could be null and is dereferenced at line 5245, column 5.
5243. */
5244. lbm_value *reserved = stack_reserve(ctx, 3);
5245. reserved[0] = ctx->curr_env;
^
5246. reserved[1] = cell->cdr;
5247. reserved[2] = APPLICATION_START;
```

But the thing is that stack_reserve should not be able to return NULL. It either returns a valid ptr or it executes a longjmp and does not return at all (at this location).

Id love to understand what is going on here. It has happened before that infer warned me about something that I was (incorrectly) sure about.

Infer version v1.1.0-e4d1723e7
Ubuntu
infer run -- make

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.