Question: Does infer know about setjmp/longjmp ?

[svenssonjoel]

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