<div dir="ltr">> How tell to checker that this block doesn't require nvlist_free or bypass<div>this return?</div><div><br></div><div>In such cases i'm usually doing stuff like:</div><div><br></div><div>- 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())</div><div>- 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()),</div><div>- add independent transitions to both newly created states (CheckerContext::addTransition()).<br></div></div>