Checker for nvlist

How tell to checker that this block doesn’t require nvlist_free or bypass
this return?

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()).