How tell to checker that this block doesn’t require nvlist_free or bypass
In such cases i’m usually doing stuff like:
- split the program state in post-call of nvlist_alloc(): assume the return value symbol of nvlist_alloc() is zero in one state and non-zero in the other state (ProgramState::assume())
- mark the symbol as allocated only in the first state (you are most likely doing this somewhere in the generic data map, aka ProgramState::set()),
- add independent transitions to both newly created states (CheckerContext::addTransition()).