I had to fish around a lot but Splint now handles thing cleanly if a global is used in a /*@requires isnull ..@*/ or similar clause.
Basically, we just ignore the variable as was the old behavior. The bug was that llassert were failing. I think things likely became broken after the code implementing the overloading of the requires keyword was added.